# Contributing

Start from a paper, not from a proposed universal ontology of physics.

For each paper:

1. archive the best available primary source under `references/`;
2. identify the physical systems, regimes, and quantities used;
3. define paper-local Lean data and proposition-valued claims;
4. state imported mathematics, physical principles, approximations, and
   calculations as explicit theorem hypotheses;
5. prove the paper's logical conclusions from those hypotheses in Lean;
6. add an auxiliary source map linking claims and transitions to the primary
   source;
7. add a total coverage interpretation from every source-map atom to the
   primary semantics or an explicit paper-local proposition;
8. prove every named route's individual inference steps and declared outputs
   using the primary semantic theorems and explicit hypotheses;
9. classify every source-mapped step by its actual epistemic strength;
10. separate independent derivations and interpretive extensions into typed
   paper-local routes;
11. independently review every public main conclusion in both hand-written
   dependency and epistemic ledgers, cover every route exactly once, and
   realize actual inhabited retained-versus-rejected countermodel boundaries;
12. extract shared infrastructure only after another paper needs it.

Opaque atoms and typed dependency graphs are useful for provenance, but they
do not count as the Lean formalization. A completed target needs substantive
theorems over semantic definitions and route certificates connecting those
theorems back to the source-mapped outputs.

In particular, do not classify a supposition introduced for contradiction as a
physical premise. Use a reductio status and preserve where that temporary
hypothesis is discharged in the paper's argument.

The archived source must include the original primary paper. Reviews, later
clarifications, lecture notes, and metadata are useful supplements but cannot
replace it.

Prefer the author's TeX source when it is available, while retaining a PDF for
stable pagination. For papers without source files, use a legitimate
publisher-, author-, or university-hosted PDF and record its bibliographic
metadata and download location. The `references/` directory is local and
intentionally gitignored; durable source mapping belongs in the target dossier.

Do not add theorem-shaped wrappers around supplied conclusions. Hypotheses
should express genuine upstream principles or calculations, and the desired
conclusion should be derived from them. Do not add global registries,
taxonomies, or metadata systems without a concrete need demonstrated by active
paper reconstructions.

## Semantic Review

The review surface includes every declaration that determines physical meaning:
definitions, structures and inherited field restrictions, inductive alternatives,
selected instances and coercions, and theorem parameters and hypotheses.
Calling a declaration central or peripheral does not change that obligation.
Proof correctness, physical faithfulness, and empirical truth are distinct.

The local pilot is `docs/review/GuthRadiationHorizon.html`. Its meaning graph
and separate proof-reference view are extracted from the elaborated environment,
not inferred from source comments or declared route metadata. Inference cards
show proposition-valued outer hypotheses jointly and retain every data and
instance parameter in the complete statement. Proof references are syntactic
dependencies, not independently sufficient premises or a historical proof route.
External mathematical bodies remain explicitly unexpanded boundaries.

Schema 7 additionally records one-step expansions of project predicates at the
head of an outer statement part, using that part's actual arguments. A kernel-
checked reflexivity application verifies the chosen expansion's definitional
equality; it is not a new theorem assumption or an independent characterization.
The original statement and forall/let context remain visible. Do not recursively
simplify these expansions, unfold external definitions, discard proof arguments
or instance bindings, or treat an expanded predicate as human-reviewed.
Older schema-4/5/6 exports remain comparable with an explicit schema-change
notice; import does not run Lean or confer review authority.

The page contains six review exercises. The original three test emission at the
limiting origin, endpoint-only speed tests, and emission-time quantifier order;
their deliberate alternatives remain in `tests/semantic_review`. The further
exercises distinguish one shared past event from worldline-to-worldline
signalling, retain the strict boundary and nonempty region, and connect the
entropy-rescaled region to one common event. Production characterizations use
actual curves, while concrete contrasting intervals remain diagnostic models.
Independent contracts cover all eight causal definitions and the exact result
signatures; twenty compiled definition mutations and nine weakened results are
rejected. These are automated contract checks, not evidence that a human has
verified the interpretation. The common-past consequences do not establish
thermalization or an inflationary history and are not additional historical
claims attributed to Guth.

`docs/review/UniformForecast.html` follows the same extraction path through
the paradigm's compatible-outcome semantics, the metric framework, and an
external consumer's actual linear flow. Its five exercises distinguish a
failed nominal forecast from failure of every uniform forecast, reject
vacuous success on empty information, and recover exact prediction from exact
initial information and unique evolution. The midpoint example retains the
strict factor-two boundary for closed error balls. These are accuracy
feasibility statements, not algorithms, error probabilities, or Lorenz's
atmospheric horizon. The added unique-successor readback separates existence
and uniqueness from stability. A discontinuous threshold iterate and the
continuous exponential mode with no uniform all-future error radius distinguish
two logically different failures of prediction. Independent contracts expand
the forecast predicates and pin seven consumer results plus the paradigm
equivalence. Eight compiled changes to the six dynamics definitions must fail
literal readbacks; deprecated names are separately checked for compatibility.
None of these automated checks is a blinded human trial.

`docs/review/DensityVariational.html` exposes all fields of the density-minimum
model and a kernel-checked expansion for arbitrary selected three-site waves
and particle-number sectors. The right-hand statement uses normalization,
the actual hopping matrix, density norm-squares, energy attainment, and the
fixed-number candidate bound. It does not assume the compound predicate it
characterizes. Five exercises cover this read-back, phase-dependent kinetic
energy at the same density, candidates outside the number sector, and the
difference between state and local-potential eigenstate representability.
The global-phase exercise additionally proves a one-dimensional ground
eigenspace and characterizes all normalized ground vectors by one unit-modulus
phase. Its sign-change control refutes literal vector uniqueness and strict
energy increase for every distinct vector, while preserving physical-state
uniqueness. This finite diagnostic does not supply continuum wavefunctions.
The last has both a uniform positive control and a boundary-density
obstruction with zero sites. This is a finite model, not a counterexample to
strictly positive continuum potential representability. Independent result
contracts and compiled negative tests remain engineering checks, not a human
read-back or an attestation that the original physics has been approved.

`tests/semantic_review/CheckDensityDefinitions.lean` separately characterizes
all 19 data and predicate declarations of that finite model. Definition-level
negative tests extract their actual source bytes into a proof-free module:
the unchanged projection must compile and satisfy the contracts, and twelve
well-typed physical alterations must compile but fail the contracts. The
alterations cover complex amplitudes, normalization, hopping, kinetic energy,
admissibility, the constrained value, model fields, and local potential action.
They also distinguish one shared unit-modulus phase from arbitrary rescaling
or site-dependent phases, and a global sign change from a local one.
These detect selected changes to the agreed specification; they do not establish
that the specification itself is physically correct or human-approved.

`docs/review/HKGroundStateQuotient.html` separately exposes the complete HK
framework's conditional quotient constructor. Five state-dependent invariance
requirements, separation and nondegeneracy up to equivalence, and imported
variational principles remain explicit. The existing paper deductions are
applied on classes, without assuming literal representative uniqueness.
Every framework field has an independent readout contract. Twelve compiled
definition mutations test wrong transfers, literal-versus-equivalence inputs,
strictness, and global-phase quantifier placement. Two normalized two-component
controls use the actual phase quotient, not an arbitrary equivalence table.
These are conditional transport and diagnostic checks; concrete continuum
domains, phase invariance and human semantic review remain open.

`docs/review/HKExactDetermination.html` factors the actual exact determination
proof through a ten-field paper-local core. It does not truncate a graph of
the full record: the public paper proofs call the smaller theorem, and a
separate checked bridge preserves every retained readout and premise.
Independent contracts cover all ten fields and eight definitions; nine
compiled definition alterations and a weakened determination theorem are
rejected. Mutation contracts use the pinned compiler with temporary artifacts
first in `LEAN_PATH`, so live production artifacts cannot mask a mutant.
The full record remains exposed by the bridge and quotient views. Smaller
specifications are not evidence of physical correctness or human approval.

`docs/review/BellCommonProbability.html` exposes the actual measure-theoretic
equations-(13)-(15) inference and the unit-direction singlet exclusion.
Independent definition readbacks cover the two data fields, outcome encoding,
normalization, measurability, response product, opposition, anticorrelation,
unit-direction domain, and singlet agreement. Definition mutations compile
without physics proofs before those readbacks are checked. Interval and
context-dependent-law controls test null-set quantifier order and the common
law assumption. They are diagnostic constructions, not models attributed to
Bell; human review and the separate EPR inference are not inferred from them.
The real spin encoding is independently compiled with just its outcome type
and real values, without the generic operations record or physics proofs.
Incorrect values must compile and then fail a literal-value readback.
A separate functional equality preserves the generic encoding; its complete
review scope still exposes that interface, while the physical exclusion's
scope does not. This is a source-level specialization, not a graph filter.
The real-valued bound uses an explicit numerical inequality; an independent
equivalence and an old-interface consumer check preserve its earlier contract.

`docs/review/OrderedMagneticLimits.html` exposes the three data fields and
actual convergence in the ordered-limit paradigm. Two production equivalences
expand the volume-first and field-first procedures into explicit positive-field
and size cutoffs, without new physical predicates or extra hypotheses.
Independent contracts cover both readbacks and all eight selected statements.
The six existing limit definitions are also compiled without physics proofs;
nine mutations of nontriviality, quantifier order, family dependence, limit
realization and agreement must compile before failing the definition readback.
The normalized two-orientation family is a diagnostic, not a Heisenberg model.
Its failure of a uniform volume cutoff, changed zero-field endpoint, and empty
approach are distinct tests. The full paper model remains inspectable in the
source-certification exercise; that model is not needed by the primary scope.

`docs/review/CalibratedMeasurementRecords.html` exposes ten statements and the
complete three-field process, including its complex-linear map types. The
four production readbacks express superposition, amplitude transport, and
nonempty record-value fibers without additional physical predicates. Literal
contracts independently pin the coefficient and record definitions; fifteen
deliberate changes must compile before failing those contracts, including
replacing either linear map with an ordinary function. Nine weakened results
must also compile before their independently stated contracts reject them.
The nonlinear diagnostic is not a proposed quantum dynamics. Agreement,
normalization, support, and definite outcomes remain separate propositions;
none of these checks establishes human semantic approval.

`docs/review/TypicalityAndJointClaims.html` exposes the three typicality
relations and the joint-state quantifier through two production theorems.
Ten compiled definition mutations test property scope, state scope, selection,
and nonvacuity. Eight compiled weakened-result trials cover the two production
results and six terminal consumer results. The generic finite canonical
weight and the bridge's exact disjointness equivalence also have independent
signature contracts. The 100-state and two-level examples are diagnostic
statistical models, not claims attributed to the original papers. In
particular, a sound and inhabited selected set need not have high measure;
the shared bridge contains no numerical probability threshold. Human review
remains pending.

`docs/review/ThermalProbeCompleteness.html` separates the actual finite
Hamiltonian, positive stationary density matrices, matrix-trace observables,
and information available through one probe. Literal contracts cover all
diagnostic definitions, including both measures and every record-context
field. Forty-seven definition mutations and sixteen weakened-result tests
must compile before independent contracts reject them. The earlier diagonal
stationarity and population-completeness results now serve as intermediate
lemmas and retain their independent exact-signature checks. A positive coherent
state has the same diagonal and all resolved autocorrelation records as Gibbs,
but a cross correlation distinguishes it and actual free evolution changes it.
The full-state positive inference additionally retains commutation with the
fixed nondegenerate Hamiltonian, as well as normalization and all three
adjacent balances. A separate route decodes diagonal entries from zero-time
noise and positive-time response of probes 0 and 2. Exact record equivalences
and conditional Gibbs identification have independent signature contracts;
the latter uses commutation without a balance hypothesis. The positivity
and noncommutation lemmas are now intermediate results with their original
exact-signature checks. The latter supports an explicit theorem excluding
certification of commutation from the Gibbs-matching records.
A positive stationary alternative matches all three equal-time records but
not the positive-time response. No physical definition was added. The view
contains forty-six statements and eight exercises; it is neither tomography
for arbitrary observables nor equilibration.
The original forward FDT is not accused of asserting its converse. Human
semantic review remains pending.

`docs/review/DGZFiniteTimeAgreement.html` exposes thirteen statements: the
common-law inference, explicit empirical-error characterizations, boundary
controls, and the complete paper specialization. Its two structures retain
all seventeen fields. Independent literal contracts pin twenty-seven
definitions; twenty-two compiled mutations exercise quantifiers, normalization,
conditioning, strictness, nonempty scope, and Born-law identification. Ten
compiled weakened-result trials test the two new readbacks, five existing
paper controls, and three diagnostic results. Signature contracts also pin the
primary inference, strict-budget existence, and paper wrapper. The quantitative
most-times estimate is a reconstruction of the source's qualitative statement,
not a formula attributed to the original paper. Human review remains pending.

`docs/review/WittenSpectralIndex.html` follows fourteen statements through the
regulated trace, complete spectral representation, actual operator pairing,
normalized charge kernel, convergence controls, and full four-charge physical
specialization. Two production equivalences expose existing meanings without
adding definitions. Independent literal contracts cover twenty-five definitions;
thirty compiled mutations test signs, trace normalization and convergence,
basis alignment, charge kernels, and ground-state order. Four weakened-result
trials cover the readbacks and two trace controls. Every mutation must compile
before its independent contract rejects it. Signature contracts also retain
the primary inference and full physical specialization, including the latter's
nonzero-index input. The main scope is not the SU(N) index calculation, and a
formal charge grading alone is not a physical rotation representation. Human
semantic review remains pending.

`docs/review/BetheTripletRange.html` follows fourteen statements separating
signed amplitude, squared readout, channel signs, coherent-sign selection,
binding kinematics, and the range-replacement error. Literal contracts cover
all eight new non-diagnostic definitions, including the record-context fields.
Seventeen compiled definition mutations and twelve weakened-result trials
exercise these distinctions and the actual paper join. Diagnostic pairs are
not claimed to arise from nuclear potentials. The printed sign in (25) stays
intact; its inconsistency check is conditional on fixed mass and hbar, not an
author-approved erratum. Human semantic review remains pending.

`docs/review/PhysicalObserverRoles.html` exposes fifteen statements separating
occupied roles, physical status, optional consciousness classification, and
interaction-produced accessible records. Literal contracts pin all eight
physical-role predicates and both forgetful-adapter fields. Compiled mutations
must reject changes to the quantifiers, required conjunctions, or consciousness
independence, while independent result signatures retain the actual Everett
calculation, interpretation, and coefficient-realization premises. The complete
adapter ties the physical post-measurement state to the same coefficient map,
requires calibration and actual supported records, and derives nonempty
pointer-fiber determination. Twelve additional compiled definition mutations
exercise the source-model identifications and support conditions. The full paper-model field inventory
must not reintroduce its unused consciousness classification. These tests and
finite assignments do not certify physical observers or human semantic approval.

`docs/review/CosmicInferenceQuantifiers.html` exposes eleven statements, separating
fixed-estimator variation, a decoder shared across unknown models, and
almost-sure recovery. Independent literal contracts pin the support, target,
estimator, two-point probability weights, readings, and decoder. Compiled
mutations exercise both the logical quantifiers and the numeric experiment;
independent result contracts retain the explicit moment input and reject
weakened sampling and decoder claims. The scalar Gaussian diagnostic is not
a finite-multipole optimality theorem; its zero-power control tests the need
for positive variance in both laws. The two-point experiment is not a
Gaussian CMB model. Neither automated check records human semantic approval.

`docs/review/ImpermeableLayerLimit.html` exposes thirteen statements about fixed
wall forcing and a singular viscous layer. The independent consumer must keep
the actual field derivatives, positive density and viscosity, both momentum
balances, continuity, impermeability, and its far-field limit inspectable.
Literal contracts pin the differential operators and physical model fields;
compiled mutations test the forcing, phase, scaling, regularity, and balance
conditions. Result contracts separate unsteady from steady equations, pointwise
from uniform limits, and wall shear from inner viscous acceleration. The
source's steady regime and the diagnostic's lack of a common initial profile
must remain explicit. These checks do not constitute human semantic review.

`docs/review/OnsagerFixedTemperatureVariation.html` exposes sixteen statements
about the source's fixed-temperature variational argument. Literal contracts
pin the two functional fields, eight spatial readout fields through their
operators and predicates, the temperature weights, actual finite resistance
matrices, and trial-flow restrictions. Compiled mutations exercise those
definitions, while result contracts reject weakened normalization and
counterexample claims. The original normalized temperature force and the
inverse-temperature gradient must not be conflated. Spatial integral
representations and Green's identity remain explicit inputs; finite matrices
are diagnostics, not fitted crystals or a complete continuum realization.
Passing these checks does not approve the physical interpretation.

`docs/review/CoarseGrainingAndClosure.html` exposes eighteen statements about
exact elimination, pairwise model closure, reexpression, and information loss.
The two-field probability projection has an explicit input characterization;
its output-law normalization and pushforward identity are derived consequences.
The finite-star witness computes its normalized marginal and generated
four-spin energy coefficient. Nonclosure is stated for probability measures,
not merely for an energy representative with its arbitrary additive constant.
Literal contracts pin the projection, canonical weights, spin observables,
energy family, and decimation maps; independent result contracts reject
weakened conclusions. The almost-sure decoder obstruction requires two non-null
states in one retained fiber. A Dirac control preserves almost-sure recovery
while rejecting pointwise recovery. Probability bounds and explicit Ising
Boltzmann kernels qualify the chain's otherwise algebraic composition law.
The original Kadanoff and Forster-Nelson-Stephen sources motivate these
distinctions; the finite witnesses do not realize their critical or interacting
regimes, supply truncation-error bounds, or constitute human semantic review.

`docs/review/HubbleDistanceCalibration.html` exposes twenty-five statements about
the angular solar correction, finite radial-fit scale ambiguity, and distance
anchors. Literal contracts pin the numerical data, positive-distance domain,
sample restriction, residual, calibration map, and fixed-weight loss. The
positive scale floor is derived when the allowed anchor error is smaller than
the reference distance. Independent controls distinguish a bounded but
nonunique coefficient from an unbounded coefficient family with unchanged
residuals. The full paper adapter and tentative epistemic status retain their
own premises and complete structures. The inspector can import one additional
trusted built module for a combined review without adding that dependency to
the independent consumer. The joint-fit extension retains the source's
angular solar projection while varying the solar coefficients. Its exact
contracts expose antipodal and same-direction decoders, nonzero distance
denominators, separate residual bounds, and a fixed-distance degeneracy when
distance follows a direction cosine. Two numerical controls use distinct
directions and distances or saturate the nonzero-residual bound; a second
compatible coefficient proves that the antipodal error bounds do not establish
an exact value. The original
control data now have a literal contract with eight additional field mutations;
four new leaf-result mutations test the complete inference boundaries. Existing
physical definitions remain unchanged; the local example data appear explicitly
in the theorem statements. These checks are not a reconstruction of
Hubble's fitting algorithm or validation of a cosmological interpretation.

`docs/review/LocalInvarianceClauses.html` exposes eleven statements separating
location changes from changes of laboratory kinematic configuration. Its
literal contracts pin all five context fields, both invariance clauses, both
comparison scopes, and the nonvacuity conjunctions. The old independent-frame
position quantifiers must compile in isolation but fail the literal contract.
The independent response `1 + a*f^2 + b*p` characterizes both sensitivities;
populated disconnected scopes refute unqualified global agreement, without
isolating availability from the comparison relation. Do not interpret the diagnostic as a counterexample to a dynamical
version of Schiff's conjecture, a test of all Lorentz transformations, or
canonical matching of tangent frames. Changed constructor meanings, matching
conventions, calibrations, and quantifier domains still require human review.

`docs/review/FrequencyReferenceControl.html` keeps fifteen source and diagnostic
statements separate. The nuclear setup's Atomichron clause must not be removed
or supplied only by the atomic branch. Independent constructor contracts expose
positive signal/reference frequencies, their quotient, actual reference access,
and finite reference allowances. Mutation tests require altered definitions
to compile before the contracts reject them; weakened result types are also
rejected. The finite bound is `d + e + d*e`, not a linearized estimate, exact
constancy, or a statistical combination of independent errors. The calibrated
record channel presupposes independent information. Its existence does not
prove the real instrument has that information or the required insensitivity.
The rank-two energy and adjacent-gap definitions have literal contracts;
positive-spectrum, single-gap, and reference-response deductions have independent
result signatures. The paper's reference controls now mean zero selected
frequency shift at every represented orientation. Both the nuclear setup and
the technical-framework adapter must retain the actual Atomichron and proton
arguments. A spin-half calculation requires an explicit physical identification
and positive Larmor frequencies before supplying the proton control. Do not
equate distinct calculated gaps with resolved instrumental peaks or infer
constant magnetic field from vanishing anisotropy response.

`docs/review/WorkSamplingTail.html` compares ordinary work variance with the
sampling demands of the exponential-work estimator. Keep the canonical
preparation, actual energy change, same-law moments, independent product law,
strict error events, nonempty sample, and finite budget visible. The diagnostic
uses thermal energy units and does not attribute its numerical values to
Jarzynski. Small ordinary variance does not imply a small exponential second
moment. The source's sufficient consistency theorem concerns that exponential
moment and eventual counts, not a prescribed affordable count. Literal
contracts and compiled mutants check the data, estimator, sampling law,
domain restrictions, and convergence quantifiers; independent result contracts
retain the actual probability inequalities. No automated result records human
semantic approval.

`docs/review/StatePositivity.html` exposes a repaired shared state predicate.
For complex-linear expectations, nonnegativity of the real part alone is not
positivity. Retain reality of every `a* a` expectation, normalization at one,
and the full observable domain. The literal contract spells out real and
imaginary components independently of the selected complex-order notation.
The two-outcome counterexample and equal-mixture control use actual linear
functionals. Projection bounds require a genuine self-adjoint idempotent;
weak-limit preservation requires a nontrivial filter and positivity of every
approximant. None of these conditions interprets an arbitrary auxiliary
ground-term field as a physical ground projection.

`docs/review/UnitaryInfluence.html` compares actual unitary preparations, not
arbitrarily assigned signal predicates. Keep the initial vector, Hamiltonian,
local operation, local self-adjoint observable, and readout maps explicit.
The generic functional bound requires contraction; the vector specialization
derives that property from normalization and preserves full positivity after
the operation. The finite two-qubit diagnostic uses the actual Hamiltonian
exponential. Its small-norm witness depends on both tolerance and candidate
velocity. Do not replace this quantifier order with one universal time, equate
suppression with zero, or describe the selected unit-separation cone as
relativistic spacelike separation. Literal definition contracts and independent
result contracts retain these distinctions.

`docs/review/PhaseMixingRecovery.html` keeps velocity integration distinct from
pointwise phase persistence and from reversible evolution. Inspect the actual
post-reversal distribution `f(T, x-v*s, -v)`, both dynamical species, positive
masses, distribution positivity, integrability, derivatives, and Poisson
closure. Recovery takes positive elapsed time after an ideal external reversal;
do not call it autonomous recurrence or the nonlinear plasma-echo experiment.
The reversal time depends on the tolerance, and the small-density bound is
uniform in position. Landau's fixed-ion source needs separate contour and
nonzero-residue inputs. A zero residue permits decay; a kinetic solution alone
does not supply Poisson closure. Literal definitions and independently stated
results must retain those distinctions.

`docs/review/LightConePropagation.html` separates the squared interval from
time orientation and from an operational signal relation. Inspect the explicit
speed-bound hypothesis, not only the predicate name `FinitePropagation`.
The source readout requires an admissible boost and calibrated times of the
same event. All seventeen fields and the paper's remaining geometry hypotheses
are visible. The coordinate diagnostic does not instantiate every abstract
paper relation. Literal contracts protect the three delegated signalling
predicates and every clause of the repaired order definition.

The paper-local `Minkowski1908/CausalCoordinates.lean` uses time and Euclidean
three-space, not a one-axis metric. Review positive c, chart bijectivity,
the two relation equivalences, and the one-way direct-light condition separately.
Null separation does not assert an available device. The source calibration
must identify all four coordinate values in the same selected frame and
strictly timelike interiors. Inspect `pastLightPoint` and `futureLightPoint`
alongside the distinct timelike points; replacing strict interiors with closed
cones would conceal the earlier conflation. Chart uniqueness is relative to
those fixed coordinate-value data, not a preferred-frame postulate. The main
geometry output requires this calibration and its signal proof uses it.
Literal contracts and compiled negative controls must preserve these choices.

The contextual field table must show every exact field type without opening a
disclosure. Local labels are the actual constructor binder names, linked to
qualified declarations; the full projection disclosure retains that qualified
identity as visible text. Binding kinds, proposition-valued restrictions,
field order, earlier-field references, and inherited structures must not be
lost to compaction. Browser tests compare both printing modes with the Lean
extraction, open every projection in representative physics structures, test
keyboard navigation, and enforce unclipped types at their existing font size
across desktop and mobile widths. Layout improvements are not semantic review.

Explicit expressions larger than 16 KiB may share repeated elaborated subterms
using local `let` bindings, with every binding value displayed. Sharing uses
structural expression equality, retains binder scope and selected instances,
and never removes proof arguments. Expansion of the shared expression must
equal expansion of the original expression structurally; the kernel also
checks the shared term. Dependencies and normal printing still come from the
original expression. Regression tests re-elaborate the printed terms and check
their equality, including shadowed binders, instances, and dependent proof
arguments. Changed explicit printing conservatively changes review fingerprints;
it does not grant or renew human approval.

Schema 5 additionally exports each stored field's type under its actual
constructor telescope. Shared constructor parameters appear once; earlier
field and instance dependencies are position-indexed and navigable. The
producer checks field positions and binding kinds against Lean's projection
metadata. Validators compare the complete contextual binder sequence and
result with the separately extracted constructor signature, so reordered
parameters cannot pass merely because their reference indices remain in range.
Full structure and projection types remain available in disclosures. Compiled
dependent-type and restriction changes exercise the contextual display, while
proposition-valued records and both diamond parents retain their constraints.
Schema-4 comparison imports are supported without inventing missing contexts or
transferring human approval. Display changes conservatively invalidate review
fingerprints; they do not by themselves establish a changed physical meaning.

`docs/review/RepresentationAndPhysicalValues.html` exposes seven statements,
including a literal expansion of nonempty soundness into all seven primitive
relations. Its thermometer decoder equivalence quantifies over every admitted
temperature and bias; exact reference subtraction, partial-domain soundness,
one correct assignment, recorded estimates, and inexact informative bounds
remain distinct. Thirteen compiled mutations test the seven foundational
definitions. Six compiled weakened-result trials test the production readback
and five terminal consumer results; the decoder equivalence additionally has
an exact independent contract, but is not counted among these trials because
the reference-correction proof uses it. This is a diagnostic of interpretation,
not a proof of empirical adequacy or completed human semantic review.

`docs/review/ResidualInference.html` exposes the measurement philosophy's
nonempty record fibers and universally quantified value constraints through
the Penzias-Wilson scalar residual. Its interval characterization includes the
nonnegative error width, not a sampling law or actual-sky compatibility.
Six exercises separate positivity from exact identification, retain
compatibility with the error budget, and test an additional bound on other
unassigned contributions. That bound plus the error width must be strictly
below the readout to force a positive cosmological remainder; an explicit
boundary example blocks the weaker comparison. The independent contracts
pin all thirteen selected statements and the underlying record specifications.
Eight compiled weakened-result trials cover the constructed diagnostic module;
the primary paper statements are checked by the separate contract file, not
counted as those eight mutations. A typed bridge also connects the component
subtraction to the residual record. Its exact uniform-error criterion includes
the sum of the three component bounds plus the absolute change of center;
nonnegative component bounds keep the box inhabited. The 0.05 K backlobe in
the numerical control is not a historical observation, and its 1.05 K recentered
radius is not a correction to the paper's uncertainty. Positivity is transferred
through actual record compatibility, not just a matching displayed number.
The spectral route now deduces exclusion from actual two-frequency temperature
ratios, not an exclusion supplied as a calculation output. Known-source
classification and spectra are independent inputs, and their comparison retains
an inhabited candidate family. A whole explanation supplies the high-frequency
residual while staying below the low-frequency sky budget. Equality at the
spectral bound does not exclude it; a smaller steep contribution can remain
within both budgets. These 2 K controls are not historical measurements.
Six definition-only mutations test frequency ordering, the primitive ratios, strictness, whole
versus partial accounting, and nonnegative low-frequency contribution against
independent Lean specifications; production proofs are absent in those trials.
The complete instrumental analysis remains outside the review slice.

The nuclear review now begins with the contact-chain order-selection argument.
Its single bookkeeping definition records C_(2n) p^(2n) at each vertex and one
loop per adjacent pair. Coupling and loop order assignments are explicit inputs;
unbounded leading dressing and the single derivative insertion are conclusions.
The normalization identity is a supporting check. Do not confuse assigned
diagram order with a nonzero asymptotic leading coefficient, convergence, or
remainder control, or claim the legacy abstract calculation contract is discharged.
Human usability and semantic approval remain open; their absence does not
prevent source-based agent review or repair of a known formalization gap.

Paper companions omit abstracts and generic process notices. Their main text
contains definitions, assumptions, equations, physical qualifications, and
source citations. Review status and source hashes remain in the extraction
metadata; displaying a declaration does not create a review record.

Every paper HTML companion includes a visible **Definitions and assumptions** inventory in
its main text. It lists the complete elaborated declaration census of the
paper's main module, helpers, source map, coverage interpretation, and fidelity
ledgers, together with their transitive project meaning dependencies. Source
mappings and interpretation choices have a separate group: Lean can check a
mapping's consistency, but cannot establish its faithfulness to the paper.
Generated declarations are retained, so the inventory count is not a count of
independent physical choices. Review pages list the union of the meaning dependencies of all their
selected statements and exercises, including statements other than the initial
selection. Their scope remains the selected arguments.
Review pages retain their argument controls and inspector first; the
**Definitions and assumptions** link near the top jumps to the complete
inventory below that interactive area, within the main text.

Click any inventory entry to open its details in the bottom panel. Relevant
Lean code appears first: the complete authored definition or structure when
its source span can be verified, or the exact elaborated specification when
an authored declaration is unavailable. Generated fields and constructors can
show their metadata-identified owning declaration. The panel does not send
readers to an entire Lean file. Source excerpts are pinned to the extraction's
source bytes; compiler declaration ranges are preferred, with a conservative
indexed fallback. Surrounding imports, namespaces, section variables and
notation may be outside the excerpt, so it is not a standalone Lean file.

The panel also retains exact types, inherited constraints, constructors,
selected instances, and all theorem parameters and hypotheses. Full theorem
proofs remain outside the meaning inventory. Dependency links open the
corresponding declaration. The explicit notation option exposes implicit
arguments; Close or Escape returns focus to the entry. Paper inventories elide
nested Lean-checked proof terms from elaborated definition bodies and label
that omission explicitly. Original definition source excerpts retain those
terms intact; toggling explicit notation does not rewrite the source excerpt.
The inventory remains visible without JavaScript. Mathematical
declarations outside the project are listed as external boundaries with their
types, without expanding their bodies.

Lean checks the formal specifications and proofs. Human review must establish
whether the definitions, domains, hypotheses, and interpretation express the
intended physics. The theorem statements in this inventory expose that review
obligation; they do not reclassify checked proofs as unproved results. No
inventory entry or successful extraction creates a human attestation.
Axioms are labeled separately as trust boundaries: they have no Lean proof
body. Generated `native_decide` axioms in source-map and coverage modules
identify the native evaluator/compiler trust boundary. Other project and
external axioms receive no compiler-origin claim. Their exact types remain
visible; listing an axiom does not classify it as an independently checked
proof or a physical assumption.

`scripts/sync_html_papers.py --write` refreshes the paper inventories from Lean.
Regenerate review pages afterward with `scripts/build_semantic_graph.py`, since
their review fingerprints include the linked paper editions. The HTML audit
compares the displayed inventory and its detail data with a fresh elaborated
census, rather than accepting a count or a self-reported cached list. Focused
regressions run with `python3 -B scripts/test_companion_inventory.py`; the
separate browser command is `node scripts/test_companion_inventory_browser.mjs
--all`, with optional `--screenshots` pointing outside the repository.

Large detail records use deterministic gzip compression inside the HTML; the
visible inventory is ordinary HTML. Opening compressed details requires a
browser with `DecompressionStream` support. Compression preserves every
extracted value, and the audit compares decoded records with fresh Lean output.
Paper extraction uses the pinned Lean toolchain's native compiler and two
isolated workers by default. Set `PHYSICSLOGIC_INVENTORY_JOBS` to an integer
from 1 to 32 when the machine has sufficient memory. Native binaries and
fingerprinted development caches live under ignored `.lake/`; standard checks
still build and extract the inventories afresh.

The **Complete project specification** tab displays the selected statement's
entire project meaning closure, not its proof implementation or the whole
original paper. Each declaration retains the same exact types, bodies, fields,
binders, recursor rules, and review status as the focused view. Strongly
connected groups keep mutual references together and place other project
dependencies before their users; their order is not a reconstruction of the
paper's reasoning. External declaration types are listed separately, with
their bodies unexpanded. Browser checks compare every displayed specification
against the extracted data for every selected statement in both printing modes.
Neither opening the view nor following its links records a human review.

Use **Write an inspection note** on a focused declaration or a complete-view
entry to record what was inspected and what remains uncertain. The notebook is
an append-only collection of observations, open questions, and suspected
mismatches, not an approval ledger or an automatic question-resolution system.
Project notes use the declaration's full meaning fingerprint; external-boundary
notes concern only the displayed type and use the entire extraction snapshot.
Changed versions need reinspection, absent declarations remain visible as outside
the current extraction, and follow-up entries never silently update older notes.
Matching fingerprints locate reader-supplied entries; they authenticate neither
their author nor their timestamp and establish no physical correctness.

Entries are stored individually in browser storage when available, avoiding
whole-notebook overwrites between tabs. File-page storage is browser-dependent;
export compact JSON for a portable backup or transfer to another page. Imports
merge without replacing entries, reject conflicting IDs and malformed data,
and never modify `semantic-reviews.json` or an extraction's review statuses.
If storage fails, the page retains new entries in memory and exposes export;
unsubmitted text survives declaration navigation but not a reload. The current
limits are 1000 entries, 8000 characters per note, and 2 MiB per export/import.
The browser suite tests actual compiled definition changes, inherited-field
changes, invalid input, stale and absent attachments, concurrent tabs, storage
failure, inert text, and mobile layout. These are tooling tests, not human review.

Structure fields follow Lean's positional field inventory, not its name-sorted
metadata table; their explicit, implicit and instance binding kinds are retained.
The parent inventory follows the `extends` order and includes both embedded
subobjects and projections reconstructed from shared fields. Both the parent
structure and its projection enter the meaning closure and review fingerprint.
Compiled diamond-inheritance fixtures check that the reconstructed parent, its
body and its inherited restrictions are reachable without inventing an extra
stored field. Schema checks cross-check positions, types and parent/field edges;
fresh Lean extraction, not schema validation alone, establishes the inventory.
The browser suite compiles this small temporary fixture using the pinned Lean
toolchain and removes it afterwards; it does not create another full build.

The statement-part disclosure maps each parameter type, hypothesis, and
conclusion to its direct elaborated declaration references and earlier
telescope binders. Inference cards link to the corresponding part; binder links
keep dependent types in scope, and declaration links expose bodies, instances,
and inherited constraints. References use positions rather than printed names.
Their union is checked against the full statement's declaration dependencies;
unknown declarations, invalid binder positions, duplicate references, missing
part maps, and incomplete declaration unions fail validation. Exact placement
within each part is checked by fresh extraction, not by that union check alone.
Compiled fixtures additionally check actual extraction, including shadowed
names, nested quantifiers, selected instances, and proof arguments in types.
These syntactic references are not proof-use edges or a minimal assumption set:
a hypothesis absent from the conclusion may still be essential to the proof.

Schema 6 additionally decomposes an outer statement prefix containing
interleaved `forall` and `let` bindings. The local-context panel preserves each
definition's assigned value and type, including unused definitions, nondependent
bindings, and defined proofs. It does not hoist definitions from inside a
conjunction, lambda, or other nested expression. Later hypotheses appear in
the inference view under this same ordered context; local definitions are not
free assumptions. Each type, value, and final conclusion has exact reference
positions and declaration links. The extractor reconstructs the closed type,
checks expression equality after let expansion, and kernel-checks the result.
This is a check of decomposition, not physical fidelity. Printed names may
change with shadowing; positions and local contexts determine reference identity.
Schema-4/5 exports remain available for offline comparison with an explicit
schema-change notice, never automatic review approval. Compiled fixtures test
value changes, proof-valued definitions, unused bindings and nested scope;
browser tests verify both printing modes, later-hypothesis navigation and the
same values in the complete specification view.

Regenerate and test it with:

```bash
python3 -B scripts/build_semantic_graph.py
python3 -B scripts/test_meaning_inspection.py
python3 -B scripts/build_semantic_graph.py --check
node scripts/test_semantic_graph_browser.mjs /path/outside/repo/screenshots
```

The browser test requires Playwright and its Chromium runtime; set
`PHYSICSLOGIC_PLAYWRIGHT_MODULE` to an installed Playwright module path when
it is not on Node's search path. It also requires `lake` on `PATH` and Python
(`PHYSICSLOGIC_PYTHON` optionally selects the executable).
Browser screenshots stay outside the repo.
The normal integrity stage runs the compiled-fixture regressions. The standard
verification runner separately checks the generated page against a fresh
module build and extraction. It compiles the review exercises and their
independent contracts in a temporary module search path, includes test-source
bytes in their review fingerprints, and audits each selected result's axioms.
Readable printing can use a different namespace without changing which module
owns a declaration. The inspector executes trusted local module
initializers to access Lean extensions; it is not a sandbox for untrusted Lean.

`docs/review/semantic-reviews.json` contains only actual human attestations.
It is currently empty. Never create a record from an agent's assessment or a
successful build. A record must identify the declaration, the displayed
fingerprint, reviewer, review date, evidence of the explicit human confirmation,
and the scope `project-meaning-with-listed-external-boundaries`. The scope does
not certify the external definitions, empirical truth, or every use of the
concept. Reviews do not automatically transfer to other declarations.
Fingerprints cover the in-project meaning closure, displayed external boundaries,
owning source modules, pinned configuration, the page's physical scope and source
explanation, its exercises, and the contents of its linked paper edition.
Changing interpretation can therefore invalidate a review even when every Lean
statement is unchanged. The renderer rejects a page context that differs from
the one fingerprinted, and refuses to display approval without versioned context.
The context is page-scoped: unrelated pages and unused source modules do not
become dependencies merely by belonging to the same repository. Owning-module
and linked-edition changes conservatively invalidate reviews, including proof-only
edits. Original reference artifacts remain covered by separate source-verification
checks, not certified by a matching review record. A stale record
is retained as history, not displayed as current approval. The record file is
human-governed evidence, not a cryptographic authentication mechanism.

Use **Compare an earlier extraction** on a review page to export its current
inspection or load an earlier export. The file is read locally, never uploaded.
Export filenames contain both the page name and snapshot prefix, since different
argument pages can share the same source snapshot.
Only the interface's unmodified compact JSON exchange format is accepted, up to
16 MiB; parsing rejects duplicate keys, unsupported schemas, duplicate names,
unresolved edges, inconsistent field/parent inventories, and incomplete selected
meaning closures. This validates supplied data, not its provenance or agreement
with an earlier Lean compilation. Keep exports with their source-verification
evidence when they are used in a real review.

Comparison includes every project specification and external boundary reachable
from the selected statement. It excludes proof-reference lists, source positions,
and review attestations; none of those can silently become human approval through
an imported file. Added/removed means entering/leaving that statement's scope,
not necessarily creation/deletion in the repository. Renaming and printer changes
can produce differences without changing mathematical meaning. Exact changed
values are displayed side by side, not summarized by an AI. Source/configuration
hash changes remain separate even when no displayed specification differs; that
case is not classified as proof-only, and does not renew a stale review.
Interpretation changes have a separate comparison panel with the exact earlier
and current text. Missing context in an older export is shown as absent, not
treated as unchanged interpretation or imported approval.

The compiled comparison regression generates two isolated Lean environments with
a changed predicate, inherited restriction, added field, and changed dependency
scope. Browser tests exercise those outputs, rejected input variants, export and
local import, literal rendering of hostile markup, pending-review preservation,
and narrow layouts. External bodies remain unexpanded, and semantic equivalence,
physical faithfulness and human approval remain independent obligations.

The graph approach is informed by the statement/proof separation and audited
missions of [Prove2Me](https://arxiv.org/html/2608.28433v2). PhysicsLogic additionally
needs to preserve physical hypotheses and source-specific interpretation, even
when those obligations are intentionally not proved mathematically.

## Verification

Treat verification as evidence about the selected automated checks, not as
approval of the physics. Schema-2 reports retain explicit assurance limits on
physical fidelity, human semantic review, and project completion, including
for a full successful run. Fidelity ledgers and source-family registrations
must be described by what was checked; their counts are not human-review
counts. Keep scoped human attestations separate and do not infer global
approval from a nonempty review ledger.

Before considering a paper target complete, run:

```bash
python3 scripts/sync_html_papers.py --write
python3 scripts/check_all.py
```

The verification runner hashes the actual input contents before running and
checks that snapshot before and after every stage, including selected-stage
runs. The scope is `PhysicsLogic/`, `scripts/`, `tests/`, `docs/`, the root
aggregator, contributor instructions, README, Lake configuration and lock,
Lean toolchain pin, and the entire selected reference archive. Set
`PHYSICSLOGIC_REFERENCE_ROOT` to select an external archive; every child process
is pinned to that same resolved archive path. Untracked files
are included; Git history is not the source of truth. Build/Python caches and
OS metadata are excluded. Nested directory symlinks fail closed rather than
silently omitting their contents; file symlinks include their target and bytes.
Any input change or unreadable input invalidates the run and requires a fresh
run on a stable tree. The log records the content digest and reference root.
These checkpoints detect observed concurrent changes, not edits restored
entirely between checkpoints; use an isolated checkout for release verification.
They do not certify tool binaries or build-cache integrity, and a selected-stage
pass is not a full-library pass. The focused runner regressions are
`python3 -B scripts/test_verification_snapshot.py`; they also run in the normal
policy-integrity stage.

The default seventeen-stage sequence checks governance keys first, then the
source, physics, build, reuse, and graph gates, and finally the exhaustive
policy-integrity regressions. The new `policy-keys` preflight supplements every
previous mandatory check. Neither it nor a selected run of `policy-integrity`
alone is a complete verification. Use stable check identifiers, not remembered
stage counts, when selecting a partial run.

The common compiled definition and theorem-mutation checks use at most two
Lean compiler workers. Every positive control and mutant is compiled afresh
in its own temporary module directory, followed by its independent contract;
a failed compilation is not counted as a rejected contract. Results are
reported in the original case order, and all workers finish and remove their
artifacts before the result is checked. Lake builds remain serial and reuse
the canonical build tree. Set `PHYSICSLOGIC_MUTATION_JOBS=1` for serial compiler
execution; only `1` and `2` are accepted. No test verdicts or mutation artifacts
are retained across runs. The integrity-stage log records the test count,
elapsed time and configured worker bound. Real serial-versus-concurrent
fixtures check verdict agreement, replacement-module precedence, failed
compilation, unchanged upstream artifacts and cleanup. These small scheduler
fixtures exercise both worker counts even when physics mutations are configured
to run serially. A rejected contract must exit normally with Lean error status
1 and the expected diagnostic; a killed compiler or another abnormal process
exit is a failed test, never evidence that a semantic mutation was caught.

Edition synchronization refreshes the Lean build and extracts actual route
records, including parameterized source maps. Every edition has a managed
checked-route appendix, and the catalog records the same ordered fields.
The independent Lean fidelity audit verifies identifiers, kinds, direct
predecessors, inference steps and outputs. Custom exposition and diagrams
remain separate: do not treat a synchronized identifier inventory as proof
that every explanatory sentence or diagram is current.

Source-fragment guards complement Lean compilation; they do not prove physical
fidelity. A target must be either a unique bare declaration name or its full
namespace-qualified name. Do not select a declaration by slicing a source file
at a namespace or structure marker. Comments, strings, and attributes cannot
supply required physical fragments.
Identifier punctuation is significant: `value`, `value?`, and `value!` are
distinct targets, including under `_root_`. Unsupported query syntax fails
closed; this lexical index is not a replacement for Lean's name resolution.

The source checker caches exact source contents and isolates closed,
single-declaration mutations. Scope-changing edits fall back to full-file
checking. When changing this machinery, run both its focused tests and the
complete differential reference check:

```bash
python3 -B scripts/test_lean_source_contracts.py
python3 -B scripts/check_policy_integrity.py --full-source-reference
```

The normal integrity stage always runs the focused tests and every registered
physical mutation; the reference option adds a full-file comparison for each
mutation. Missing, ambiguous, stale, and unchanged mutation targets are errors,
not skipped tests.

The production policy also checks compiler-parsed import headers and
transitive layer boundaries, including unregistered and nested helpers.
Use `python3 -B scripts/check_import_layers.py` for the focused check and
`python3 -B scripts/test_production_source_discovery.py` for its regression
tests. Header parsing uses the installed pinned Lean toolchain, batches
uncached source texts, and neither resolves fixture dependencies nor executes
their commands. Comments cannot introduce imports, and parser failures never
count as an empty dependency graph.
Project module names must match discovered source paths exactly. Quoted
filesystem paths, parent traversal, and case aliases cannot substitute for
canonical imports, even on filesystems where Lean could resolve such aliases.

The `external-consumer` stage builds `tests/consumer` as a separate temporary
Lake package, using the library's pinned Mathlib revision and exact locked
dependencies. Its physics proofs import only public framework/foundation
modules. Their elaborated dependencies must use the specified public APIs,
contain no paper-module or canned-countermodel shortcuts, and depend only
on Lean's three permitted foundational axioms. Run it independently with
`python3 -B scripts/check_external_consumer.py`; generated artifacts remain
outside the source fixture.
When changing dependency indexing, also run it with `--compare-reference`
to compare present and absent public-API dependencies against fresh Lean
collector traversals. This option requires a build, not `--check-only`.

The standard command rejects duplicate Python governance-policy and
primary-source-portfolio JSON keys, independently inventories every elaborated
production declaration (including generated theorems and unused axioms), cross-checks attributed
source `theorem` and `lemma` declarations, and checks that each
foundational module has at least two
direct downstream clients whose elaborated declarations actually use its
semantics. Every domain-neutral foundation must also have actual elaborated
dependencies from primary-paper formalizations with source and fidelity ledgers
in at least two registered physics families; a single-family exception is
allowed only for a physically specialized paradigm with a recorded scope
justification. Every active philosophy module and each registered general
paradigm must have actual elaborated clients in at least three registered
physics families. These registration and use checks do not validate the
physical interpretation of a definition or the accuracy of a family assignment.
It also checks that every shared
technical framework has at least
two independently authored primary-paper clients and an actual elaborated
proposition-valued `Nonvacuous...` physical-result definition used by at least
two independent primary-paper clients. Every framework-to-framework
composition must also use the imported child's actual elaborated
`Nonvacuous...` physical-result definition. Every non-auxiliary production
declaration must remain free of compiler-generated proof axioms.
Compiler-assisted finite decisions are permitted only inside named theorems
of an exact paper `SourceMap.lean` or `Coverage.lean` module, with separate
audits for provenance and semantic-route coverage; neither may flow into
foundations, technical frameworks, primary paper results, or fidelity
certificates. Add
`--legacy-axiom-trace` only when the substantially slower verbose
declaration-by-declaration trace is needed.

For a source-only checkout, set `PHYSICSLOGIC_REFERENCE_ROOT` to the separate
local primary-paper archive. Both provenance checks and policy-level original
source comparisons use that location without requiring archived PDFs or TeX
bundles in the published checkout.