Lean

Lean formalization workspace

This is the umbrella Lean 4 / Mathlib project for the repository. It contains a sorry-free proof subset covering finite observer consensus, public records, normal forms, coupling algebra, the screen/trichotomy arithmetic, and the exact algebraic/compositional kernel of the typed Einstein branch. It also checks the finite de Sitter capacity-transfer identities, the eigenvalue signs of the declared analytic Hessian action, and the pure-de-Sitter shock normalization. The source contains no admitted proofs. Thirteen finite proofs use native_decide, whose generated native-code evaluation axioms are tracked by tools/check_lean_native_decide_inventory.py; the other audited proofs state their axiom dependencies in their module reports. Continuum geometry, asymptotic tails, physical identification, and existence of an Einstein-admissible source tower are explicit premises rather than proved facts.

The computation library also contains one fixed generated-node federation whose input is carried by preserved initial-state ports. Canonical genuine repairs terminate by a dependency-order rank, while pathwise weak fairness upgrades stuttering attempt stabilization to consensus. The historical weak repair relation is unchanged and has an explicit fair-stuttering no-go.

The observer-dynamics modules also provide exact finite witnesses for the stationary four-cycle repair generator and its Green–Kubo matrix, arbitrary survival-cocycle tilt, and a temporal-filter integrand inequality. The geometry library checks finite layer-parity quadrature, uniform-read clock separation, the rational finite-window conformal-clock control, and finite Fourier factorization for the golden orbit. Their precise scopes and source hashes are checked by:

python3 ../evidence/observer_dynamics_20260925/lean/verify.py --check
python3 -m pytest -q ../evidence/observer_dynamics_20260925/lean/test_verify.py

The verifier pins the local dependencies and Lake configuration and compares compiler version and source commit across platforms. Check mode preserves the saved compiler provenance and axiom log. The six mutation tests reject changed compilers and proof pins while accepting the same compiler on another architecture.

The stochastic central limit theorem, the continuum integral behind the conformal-clock polynomial, the fixed-mode Fourier asymptotic and physical source identification are analytical statements or remaining assumptions; they are not supplied by these finite Lean witnesses.

The source/readout interface modules separate finite implications from their physical interpretation:

Module	Formal scope
Geometry/NativeGeometricSourceIdentification.lean	Fixed geometry along repair histories, zero geometric covariance, unselected volume gain and distinct finite covariance shapes
Screen/CommonHistoryFeedback.lean	Exact classical record restoration, its error amplification and finite triangular accumulation
Geometry/SourceActionMeasure.lean	Normalized action-measure uniqueness, calibration identities, density error bounds and kinetic/metric-volume separation

The associated observer-like software patches expose local state, ports, readback, retained records and supplied control operations. Their executable interfaces are indexed in the reproduction guide. Finite local-force quantum preparation is an additional analytical certificate in source_scalar_preparation; it does not supply a native vacuum, Born readout or physical clock.

Layout

One Lake workspace, nine Lean libraries across their source directories:

Lean/
├── ObserverPatchHolography.lean        umbrella module of the main library
├── ObserverPatchHolography/            main OPH library: carrier, repair,
│   ├── Bridges/                        consensus, coupling algebra, collar
│   └── EinsteinBranch/                 chain, Einstein-branch kernel
├── EventAlgebra.lean
├── EventAlgebra/                       neutral finite event algebras
│                                       (journal artifact, Mathlib-only)
├── Thermodynamics/                     finite repair thermodynamics,
│                                       stationary/nonreversible H-theorem
│                                       interfaces, reversible transport, graph diffusion,
│                                       and Einstein first-law premise links
├── Screen/                             OPHScreen library: icosahedral screen
│                                       arithmetic, A5 corpus, trichotomy
├── Dynamics.lean
├── Dynamics/                           OPHConstruction reusable dynamics
│                                       interfaces
├── InformationProjection.lean
├── InformationProjection/              conditional finite-history projection
├── Time/                               time/order type ledger and explicit
│                                       realization-map boundary
├── Tower.lean
├── Tower/                              timeless consensus tower, literal
│                                       public quotient, and conditional endpoint
├── Geometry.lean
├── Geometry/                           C1 Hermitian Lorentz module plus the C2
│                                       algebraic event/frame/celestial/rest soldering,
│                                       source-derived finite 1+3 carrier and
│                                       conditional causal-placement bridge
├── QFT.lean
├── QFT/                                conditional finite regional-net and
│                                       restriction-gluing interfaces on declared
│                                       subregion families without a coverage law
├── Locality.lean
├── ObserverPatchHolography/Locality/    fixed-word locality helpers
├── Variational.lean
├── Variational/                         scalar variational helpers and bridge
│                                       obstruction
├── ObservableNormalForms/              standalone neutral submission package
│                                       (own lakefile; also built here)
├── docs/                               proof indices and application notes
├── Main.lean
├── lakefile.lean
├── lake-manifest.json
└── lean-toolchain

ObserverPatchHolography.lean is the public umbrella module. It retains Jonathan Hill's OPH development, re-exports the separate ObservableNormalForms namespace, and imports a small bridge showing how the generic boundary-identification theorem specializes to the concrete local-repair interface.

The neutral submission project remains a single canonical source tree. To prepare its archive, zip the contents of ObservableNormalForms/; the outer repository path is not part of the archive.

Build

cd Lean
lake exe cache get
lake build

The proof receipt is the library build above. The tiny console entry point is optional and requires a native executable build (lake build oph:exe).

The neutral submission artifact also builds independently:

cd Lean/ObservableNormalForms
lake exe cache get
lake build

Its .lake/packages is a symlink into the umbrella project's package directory, so the shared Mathlib checkout is reused when building locally; continuous integration recreates it as a real directory.

Documentation

• docs/PROOF_INDEX.md: proof-to-paper mapping and formalisation status
• docs/LIBRARY_GUIDE.md: scope and module guide for the main library
• docs/EINSTEIN_BRANCH_INDEX.md: Einstein-branch statement audit
• docs/B4_LOCALITY_BOUNDARY.md: fixed-word locality and physical boundary
• docs/B5_WARD_BRIDGE.md: finite continuity and Ward-premise boundary
• docs/B7_HISTORY_BRIDGE.md: conditional history helpers and interface no-go
• docs/B8_TRANSPORT_KERNEL.md: finite Green--Kubo and graph-transport boundary
• docs/A1_TIME_ORDER_LEDGER.md: distinct time/order types, explicit bridge API, and affine clock-gauge boundary
• docs/A3_CONSENSUS_TOWER.md: directed finite tower interface, constant projective-partition adaptor, and E1/E2 wiring boundary
• docs/A4_PUBLIC_WORLD_ENDPOINT.md: literal public quotient, descended OPH endpoint, conditional schedule/representative independence, and E2 handoff
• docs/B1_PUBLIC_RECORD_ALGEBRA.md: exact active-label record algebra, sharp no-cloning theorem, and mixed-state adapter boundary
• docs/B2_PUBLICIZATION_DYNAMICS.md: normalized Kraus data, solvable publicization semigroup, literal bounded-operator exponential, fixed algebra, and physical-channel boundary
• docs/B3_PUBLIC_PRIVATE_DYNAMICS.md: stochastic public maps, exact public star-automorphism classification, the continuous public-flow obstruction, full-private-block innerness, and the open central-block and converse-generator boundaries
• EventAlgebra/FiniteBornFrame.lean and ../code/born_frame/README.md: exact twelve-port context/Born rank gap, conditional tomography uniqueness, and the source-produced public-effect boundary
• EventAlgebra/FiniteEffectClosureBoundary.lean: exact continuous nonlinear antipodal binary-weight countermodel and the dense-positivity-after-affinity closure theorem; continuity and binary normalization alone do not derive Born affinity; see docs/B13_EFFECT_CLOSURE_BOUNDARY.md
• docs/C1_CANONICAL_LORENTZ_MODULE.md: intrinsic Hermitian Lorentz module, set-level celestial quotient, frame/rest-space geometry, and exact Einstein coordinate bridge
• docs/C2_EVENT_FRAME_SOLDERING.md: bounded affine/Lorentz overlap-cocycle soldering, quotient descent, exact source 1+3 carrier, conditional order-faithful finite causal placement, candidate source-frame/rest-fiber bridge, and the remaining hypotheses for any physical refinement or smooth-manifold limit
• docs/E1_FINITE_CAUSAL_OBSERVER_NET.md: conditional finite regional-net and restriction-gluing interface, its parameterized commutative consistency model, and the open coverage, factor-localization, and noncommutative/source realization receipts
• docs/BRIDGE_BOUNDARY_INDEX.md: cross-paper boundary map
• docs/BOUNDARY_FIBER_APPLICATION.md: #304 application note
• ObservableNormalForms/README.md and its PROOF_INDEX.md: manuscript coverage of the neutral submission package