Research-Stack/6-Documentation/docs/GEOMETRIC_SUBSTANCE_CANONICAL_RECONCILIATION.md

Geometric Substance — Canonical Reconciliation

Status: Canonical. This document supersedes the scattered and conflicting usage spread across VOCABULARY_LOCK.md, NotationNomenclatureRegistry.md, the otom/docs/* conceptual notes, and the individual Lean docstrings. Where a term has carried multiple expansions across conceptual revisions, the entry here is defined by mechanism, not by label, and the superseded labels are recorded so older documents remain traceable.

Reading rule (project-wide): labels in the legacy stack are unreliable — they were assigned across many revisions and by an automated labelling pass. Trust the mechanism (the Lean definition, the proven theorem, the formula), not the name. Every claim below is tagged with an evidence tier in §7.

---

1. The geometric substance

The object the system manipulates is a single covariant geometric datum on a fixed model space, viewed through many projections. The model space is

ℂ⁸  ≅  ℝ¹⁶   with complex structure J   (a U(8) / Kähler G-structure)

This is not an interpretation imposed from outside — it is what the code builds. Law15_Field.goldenSpiral16 acts block-diagonally on 8 complex planes, each block [[a,−b],[b,a]] with λ = a + ib = φ⁻¹·e^{iθ_g}, and it is admitted only because complex-scalar multiplication commutes with J ("passes the conformal Kähler gate"). The negative controls confirm the intent: shear16 is rejected (non-orthogonal) and complex conjugation is rejected because CᵀJC = −J (anti-holomorphic).

The geometry is Cartan geometry, not Riemannian. The dictionary:

Cartan role	Realization in the stack
connection	polarity accumulator B along braid strands
curvature / torsion	braid residual R_ij = B_ij − (B_i + B_j) (BraidDiatCodec Layer 3)
development onto the model	golden contraction s' = c + φ⁻¹·(s − c), with ‖Sᵗs − c‖ = φ⁻ᵗ‖s − c‖ (PistSimulation §8)
G-structure admissibility	the conformal Kähler gate — preserve J (Law15_Field); this is the FAMM filter

The geometry carries intrinsic torsion: the super left-invariant forms are not closed, so R_ij ≠ 0 is torsion rather than an optional add-on. This is the load-bearing reason the model is Cartan (torsionful) and not Levi-Civita (torsion-free). The torsion residual is a five-channel bracket (lower, upper, gap, κ, φ), carrying an explicit curvature channel κ and a phase channel φ.

The super extension. The odd / graded directions come from the chirality flag (left / right / achiral, BraidDiatCodec Layer 1) and the eigensolid's (2k−1, 2k) coordinate pairing (BioSight G3), which is a ℤ/2 grading. Whether the grading is genuinely super — Grassmann-anticommuting, picking up the (−1)^{deg·deg} sign — is a design decision, not a fact already in the code. If imposed, the super-Cartan torsion-constraint and cocycle machinery is inherited; if not, the structure stays plain graded. The bosonic Kähler base is

---

2. The observer / observerless duality

The stack is the Observerless Research Stack: truth lives in receipt-bearing, invariant-preserving events, not in any privileged frame. Law17_Observer makes this exact — the observer is a typed projection, not an agent:

"The observer is not a separate agent but a typed projection: Π₁₆→₃ applied to the object. The measurement residual tracks what was lost in projection."

So:

• Observer = a choice of projection Π (an ObserverGate, or an orientation in SO(n) per ObserverAngle). It produces one locality-specific shape: the projected silhouette of the object (cube-along-the-diagonal → hexagon).
• Collapse residual ε_collapse = ‖M_before − M_after‖ — the mass Π discards. Aligned angles minimize it; the aligned angle reveals the object's minimal intrinsic dimension.
• Observerless = the covariant object that is true across all Π — the frame-free invariant, i.e. the equivalence class under the structure group. The "observerless-observer symbol" is Π itself stripped of any subject: an observation with no one behind it.

"Covariant geometries in locality-specific shapes" is exactly this: one invariant object, the structure group acting on it, many projected shapes.

---

3. The Sidon mirror (the inexact reflection)

For a Sidon set S, the mirror-translation c − S is again Sidon and — the key fact — has the same difference set:

D(c − S) = { (c − s_j) − (c − s_i) } = { s_i − s_j } = −D(S) = D(S)

because the difference set is reflection-symmetric. Therefore:

• At the observerless level (autocorrelation / difference structure / Fisher invariant), S and its mirror are exactly identical.
• At the observed level (any projected shape), they differ — and the difference is exactly the collapse residual ε_collapse(θ), which vanishes only when the observer-angle θ aligns with the reflection axis.

This is the precise content of "a mirror translation, a not exact one": exact in the covariant object, inexact in every projection, mediated by Π. The chirality flag (left / right / achiral) is the discrete ledger of it — achiral marks the angle where the mirror is exact, left/right mark the inexact pair seen off-axis. Chirality is not merely an address bit: the GWL coupling w_ij = cos(Δθ)·cos(Δφ)·(1 − 2|Δχ|)·exp(−|Δp|²/2σ²) carries the chirality difference |Δχ| as a first-class coupling term.

In the Cartan frame this is the standard fact, not a special case: a symmetry of the model G/H need not be a symmetry of a given realization — it holds only up to the structure group, exact covariantly and inexact in a fixed frame, with the residual measuring frame misalignment.

The golden angle. ObserverAngle says the aligned angle reveals minimal dimension and exact symmetry. The golden angle θ_g from PhiNUVMAP is the maximally mis-aligned orientation — the most-irrational angle, aligning with no rational symmetry axis. It is the least-privileged viewpoint, the angle that refuses to pick a frame: the closest realization of an observerless observer as an actual angle. This is why the golden contraction is the natural generic probe.

Incoherence as the shared resource. The same principle appears in three categories, and is the spine of the whole program:

category	instance	the resource
additive	Sidon set (distinct pairwise sums)	flat autocorrelation
geometric	high-dimensional sphere (near-orthogonality, Ma–Shen–Xie 2025)	clique suppression
dynamical	golden angle (Weyl equidistribution)	resonance / collision avoidance

The golden ratio appears because θ_g is provably the maximal-incoherence rotation (continued-fraction theory), not by analogy.

---

4. Vocabulary lock

Defined by mechanism. "Superseded labels" are recorded only for traceability to older revisions; do not use them.

Term	Canonical role (mechanism)	Locus	Superseded labels
DIAT	Integer address by perfect-square shell: k = ⌊√n⌋, a = n − k², b = (k+1)² − n. Provably bijective (encode_decode_roundtrip).	BraidDiatCodec.lean	"Dynamic Integer-Address Transform", "Dual-Interval Algebraic Transform"
PIST	The imperfect-square witness / audit surface; conserves mass = t·(2k+1−t) under lawful transitions.	PIST/*, ARCHITECTURE.md	"Perfectly Imperfect Square Theory" (keep as flavor; the role is the witness surface)
NUVMAP	Non-uniform projection onto a spectral / address coordinate surface (more resolution on important regions). Not a proof engine.	NUVMAP_NAMING_AND_DEFINITION.md	"Virtual Memory Address Projection", "Variable Mapping", "spectral container"
PhiNUVMAP	NUVMAP lifted to ℂ⁸ (16D) golden-ratio fractal coordinates with J; development = φ-contraction.	PistSimulation.lean §8, Law15_Field.lean	—
eigensolid	The pairwise-averaging fixed-point map C(p)_{2k−1} = C(p)_{2k} = (p_{2k−1}+p_{2k})/2; convergence is a compressor requirement. Distinct from NUVMAP — it is the merge on the surface, not the surface.	BioSight G3, BraidTreeDIATPIST.lean	(often conflated with "NUVMAP merge")
braid residual	R_ij = B_ij − (B_i + B_j) — discrete curvature/torsion, 5-channel (lower, upper, gap, κ, φ).	BraidDiatCodec.lean Layer 3	—
TreeDIAT	Tree-embedding score for routing/pruning plus a homeomorphic-embedding certificate (Kruskal WQO). Score routes; only the embedding proof certifies.	TreeDIATKruskal.lean	—
chirality	Mirror-handedness ledger (left / right / achiral); first-class coupling term `(1 − 2	Δχ	)`.
observer / Π	A typed projection (no agent); ε_collapse = ‖M_before − M_after‖ is the projection loss.	Law17_Observer.lean	—
observerless	The covariant object true across all Π — the frame-free invariant.	stack-wide (ARCHITECTURE.md)	—
FAMM	Admissibility filter = G-structure preservation (the Kähler J gate).	2-Search-Space/FAMM, Law15_Field.lean	"Frustration Aligned Memory Management"
corkscrew bridge	The φ-mediated interleaving of DIAT shells through the ℂ⁸ Kähler development. Projection: treeDIATToPhiNUVMAP. Contraction: phiContract. Recovery: φ⁻ᵗ = Fₜφ − Fₜ₊₁ (theorem target, see §9).	PistSimulation.lean §8, BraidDiatCodec.lean §1	—

---

5. Mechanism → port role

For folding the legacy mechanisms into BioSight / SilverSight (the port spec):

1. R_ij braid residual → curvature/torsion operator. Replaces BioSight's degree-±1 proxy and SilverSight's hardcoded nuvmap_spectral_driver.py diagonal; computed from the real graph, carrying the 5-channel bracket.
2. phiContract + goldenSpiral16 → development + admissibility. Replaces BioSight's ad-hoc G1 contraction λ = 1/√(1+B) with the φ⁻¹ golden contraction (proven φ⁻ᵗ law); FAMM admissibility = the Kähler gate.
3. TreeEmbeds + certificate → separation metric with rigor gate. Parse-tree (τ-block) separation; scalar score routes, the embedding proof certifies. No claim is promoted without an embedding witness.
4. DIAT encode_decode_roundtrip → invertibility receipt. The proven bijection is the receipt_invertible requirement, made formal.
5. Corkscrew bridge → dimensional interleaving receipt. The DIAT→PhiNUVMAP projection, golden contraction, and DIAT recovery together form the dimensional interleaving that allows lossless traversal across scales (see §9).

---

6. The Laplacian resolution

Long-standing open question: does spectral binning eigendecompose the plain graph Laplacian or the sheaf Laplacian? With the model space fixed as Kähler (ℂ⁸, J), neither: the natural operator is the J-compatible complex / Dolbeault Laplacian, the one that respects the structure the development map preserves. The geometry selects the operator.

---

7. Evidence tiers

Using the stack's own promotion ladder (RAW_IDEA → SANITIZED_METAPHOR → TOY_MODEL → TYPED_MODEL → RESIDUAL_TESTED → COST_ACCOUNTED → PROOF_CANDIDATE → CORE_MODULE):

Proven (Lean theorems — PROOF_CANDIDATE / CORE_MODULE). DIAT encode_decode_roundtrip bijection; PhiNUVMAP φ-contraction law; goldenContractionEnergyDecrease dissipation; goldenSpiral16 passes conformal Kähler gate; TreeEmbeds node/leaf monotonicity; Law17 collapse-residual; Q0_2 codec round-trip lemmas (native_decide). These are not in question.

Sound reading (TYPED_MODEL — mathematically defensible synthesis, not yet proven in-repo). The Cartan dictionary of §1; the Sidon-mirror result of §3 (the difference-set identity is a theorem; the observerless-exact / observer-inexact framing is the reading of it); the golden-angle = least-privileged-frame identification; the Dolbeault-Laplacian resolution of §6; the corkscrew interleaving description of §1 — the algebraic identities exist, the bridge theorem that wires them into a single phiContract_recover claim is the target of §9.

Stack-flagged speculative (TOY_MODEL / RAW_IDEA — the stack's own bars). ObserverAngle compression (Toybox, "not for production until 6.5σ", speculative-materials/ObserverAngleCompression.md); higher super-Cartan cohomology (cocycles / definite forms / brane molecule — nLab itself says general super-Cartan "remains to be explored"); the super/odd anticommutation decision of §1; the differential "something rather than nothing" number, which is specified but not yet computed.

---

8. Open threads

• The Sidon-mirror test. Predicted: for a Sidon set, ε_collapse(θ) has a sharp zero at the reflection axis and a positive floor elsewhere; a random (non-Sidon) sequence gives a flat curve. The depth/sharpness of that notch, against the random baseline, is the concrete "something rather than nothing" number for §3.
• The super/odd decision. Impose Grassmann anticommutation on the odd block, or keep it plain graded.
• The differential number. phi.encode_phi over Corpus250 vs a matched S⁷ null, measured against the G2 bound, wrapped as an ErdosHarness-style receipt.
• Lock adoption. Propagate this vocabulary into the repo docs, retiring the superseded labels in §4.
• The corkscrew bridging theorem. State and prove phiContract_recover in Lean: given a DIAT coordinate (k, a, b), a contraction center c ∈ ℂ⁸, an iteration count t : ℕ, and a chirality χ : {left, right, achiral}, applying phiContract t times and then recovering via the inverse golden expansion φ⁻ᵗ ↦ Fₜφ − Fₜ₊₁ preserves the DIAT shell parity and mass up to the receipt ledger. This is the theorem that wires the proven pieces (DIAT roundtrip, goldenSpiral16 admissibility, phiContract law) into a single lossless-bridge claim. Evidence target: PROOF_CANDIDATE. See §9 for the statement.
• Compliance automation. Implement the vocabulary linter and CI gates described in §10. The compliance manifest STANDARDS.toml is the single point of truth for term definitions, loci, evidence tiers, and deprecation status.

---

9. The corkscrew bridging theorem (target statement)

The corkscrew is the bridge between the discrete DIAT combinatorics and the continuous Kähler development. It is not yet a proven Lean theorem — it is a target statement at the TYPED_MODEL evidence tier, with all constituent pieces already at CORE_MODULE or PROOF_CANDIDATE.

9.1 The data

Let a corkscrew state be a tuple:

(k, a, b, χ, t)   where:
  k : ℕ            — DIAT shell index (k ≥ 0)
  a, b : ℕ         — DIAT offsets, satisfying a + b = 2k + 1
  χ : Chirality    — {left, right, achiral}
  t : ℕ            — iteration count (golden contraction steps applied)

with the conserved mass m = a·b (the PIST witness) and the chirality-dependent parity p_χ = (1 − 2|Δχ|) from the GWL coupling.

9.2 The forward map

forward(k, a, b, χ, t) =
  let c := center(k, χ)          -- shell-and-chirality-dependent anchor in ℂ⁸
  let s₀ := diatToPhiNUVMAP(k, a, b, χ)   -- projection (PistSimulation §8f)
  phiContractN(s₀, c, t)                  -- t golden contraction steps

The phiContractN applies S = φ⁻¹·R(θ_g) block-diagonally on 8 complex planes (Law15_Field.goldenSpiral16), so the forward image lives in ℂ⁸.

9.3 The recovery map

recover(s_t, c, t) =
  -- s_t ∈ ℂ⁸ is the contracted coordinate
  -- c ∈ ℂ⁸ is the original center
  -- t is the iteration count
  let s₀' := c + φᵗ·(s_t − c)              -- inverse golden expansion
  where φᵗ = Fₜφ + Fₜ₋₁  (the Fibonacci-power identity)
  let (k', a', b', χ') := phiNUVMAPToDIAT(s₀', c)
  -- verify: k' = k (shell preserved), a'·b' = m (mass preserved),
  -- χ' = χ (chirality preserved when aligned)
  (k', a', b', χ')

9.4 The theorem target

theorem corkscrew_roundtrip (k : ℕ) (a b : ℕ) (χ : Chirality) (t : ℕ)
    (h_shell : a + b = 2*k + 1)
    (h_valid : a ≤ 2*k ∧ b ≤ 2*k) :
    let m := a * b
    let s_t := forward(k, a, b, χ, t)
    let (k', a', b', χ') := recover(s_t, center(k, χ), t)
    k' = k ∧ a' * b' = m ∧ χ' = χ :=
by
  -- The proof would use:
  --   1. φ⁻ᵗ·φᵗ = 1  (from φ⁻¹ = φ − 1 and the Fibonacci identities)
  --   2. goldenSpiral16 passes the Kähler gate (Law15_Field theorem)
  --   3. DIAT encode_decode_roundtrip (BraidDiatCodec theorem)
  --   4. goldenContractionEnergyDecrease (PistSimulation theorem)
  --   5. The chirality invariance under J-compatible rotations
  --
  -- Each piece is individually proven. The gap is the single theorem
  -- that composes them.

9.5 What the theorem buys

If proven:

1. Lossless dimensional traversal. The corkscrew is invertible — the φ-algebra provides the recovery map, and the receipt format (k, t, χ) is sufficient for reconstruction. This is the analogue of Livnium's group-theoretic reversibility, but over an infinite state space rather than 24 elements.

2. Conservation law that constrains the problem domain. Unlike Livnium's ΣSW (which is the same for Shakespeare and random noise), the corkscrew roundtrip imposes a fidelity constraint: any compression pipeline that uses the golden contraction must preserve (k, χ, t) to be invertible. This is a constraint on the compressor, not just on the container.

3. Bridge certification. The DIAT→PhiNUVMAP bridge becomes a CORE_MODULE claim, not a TYPED_MODEL reading. Every mechanism in this document that depends on the corkscrew (dimensional interleaving, lossless recovery, the φ-specificity argument) is upgraded from "sound reading" to "proven."

4. Receipt schema. The receipt format for any operation using the corkscrew is minimal and fixed:

   corkscrew_receipt = {
     shell_k     : ℕ,      -- DIAT shell index
     chirality   : {L,R,A},-- mirror handedness
     steps_t     : ℕ,      -- contraction steps applied
     mass_m      : ℕ,      -- conserved mass a·b (verification check)
     center_hash : hash    -- which center c was used (anchor identity)
   }
   

   This is the receipt_invertible requirement from ARCHITECTURE.md, made specific.

9.6 Evidence tier assessment

Component	Current tier	Needed for corkscrew roundtrip
DIAT encode_decode_roundtrip	CORE_MODULE	Already sufficient
goldenSpiral16 Kähler admissibility	CORE_MODULE	Already sufficient
goldenContractionEnergyDecrease	PROOF_CANDIDATE	Energy bound is useful but not the main claim
phiContract definition	CORE_MODULE	Already sufficient
phiNUVMAPToDIAT (inverse projection)	does not exist	Must be defined
Fibonacci-power identity φ⁻ᵗ = Fₜφ − Fₜ₊₁	TYPED_MODEL	Must be stated and proven in Lean
Chirality invariance under J-compatible rotations	TYPED_MODEL	Must be stated and proven
corkscrew_roundtrip	target	Composes the above

---

10. Standards compliance structure

The vocabulary lock of §4 and the evidence tiers of §7 together imply a compliance framework that does not yet exist in automated form. This section specifies it.

10.1 Compliance manifest

A single file STANDARDS.toml at the repo root listing every canonical term, its definition by mechanism, its Lean locus, its evidence tier, and any superseded labels. Example:

[standard.DIAT]
canonical = "k = floor(sqrt(n)), a = n - k^2, b = (k+1)^2 - n, bijective"
locus = "Semantics.BraidDiatCodec"
check = "theorem ChiralityDIAT.encode_decode_roundtrip"
evidence_tier = "CORE_MODULE"
supersedes = ["Dynamic Integer-Address Transform", "Dual-Interval Algebraic Transform"]

[standard.goldenSpiral16]
canonical = "phi^{-1} * R(theta_g) block-diagonal on 8 complex planes, J-compatible"
locus = "Semantics.HCMMR.Law15"
check = "theorem goldenSpiral_passes_conformal AND theorem goldenSpiral_gate_admits"
evidence_tier = "CORE_MODULE"

[standard.corkscrew_bridge]
canonical = "DIAT to PhiNUVMAP projection + golden contraction + DIAT recovery"
locus = "Semantics.PistSimulation (s8) + Semantics.BraidDiatCodec (s1)"
check = "theorem corkscrew_roundtrip"
evidence_tier = "TYPED_MODEL"
target_tier = "PROOF_CANDIDATE"

[standard.shear16]
canonical = "I + E_01 - negative control for Kahler gate"
locus = "Semantics.HCMMR.Law15"
check = "theorem shear_fails_kahler"
evidence_tier = "CORE_MODULE"

A second table records deprecations:

[deprecated."Dynamic Integer-Address Transform"]
replaced_by = "DIAT"
migration = "Replace all occurrences with 'DIAT'. See STANDARDS.toml [standard.DIAT]."
deprecated_since = "2026-06-26"

[deprecated."Frustration Aligned Memory Management"]
replaced_by = "FAMM (G-structure admissibility filter)"
migration = "FAMM is now defined by mechanism: the Kahler J gate. Update docstrings."
deprecated_since = "2026-06-26"

10.2 Vocabulary linter

A pre-commit hook that scans .lean, .md, .py, .rs, and .pist files for superseded labels and flags them with the replacement term and the migration path from the deprecation table. Implementation sketch:

# scripts/lint_vocabulary.py
# Reads STANDARDS.toml, builds a regex trie of deprecated labels,
# scans all tracked files, emits warnings with suggested replacements.
# Exit code = number of deprecated labels found (CI fails if > 0).

This is essential because the repo is too large (700+ Lean modules, dozens of .md and .py files) for manual vocabulary propagation. The linter makes the vocabulary lock self-enforcing.

10.3 CI gates per evidence tier

The current lake build (3,314 jobs, 0 errors) covers the full workspace but does not distinguish evidence tiers. The compliance structure adds tiered gates:

Gate	Trigger	What it checks	Failure mode
G0: syntax	Every push	lake build on all files	Code does not compile
G1: core invariants	Every push	lake build on CORE_MODULE files + #eval witnesses	Core math is broken
G2: vocabulary	Every push	lint_vocabulary.py exit code = 0	Deprecated labels in use
G3: promotion	On PRs changing evidence tiers	Statement matches STANDARDS.toml; PROOF_CANDIDATE claims have Lean theorem statements	Tier claim unsupported
G4: compliance report	Nightly / release	Full make compliance output	At least one standard has drifted

10.4 Compliance report

A make compliance target that reads STANDARDS.toml, checks each standard's check field against the current codebase, and produces:

STANDARDS COMPLIANCE REPORT -- 2026-06-26

CORE_MODULE  (8/8 passing)
  [OK] DIAT               encode_decode_roundtrip            Semantics.BraidDiatCodec
  [OK] goldenSpiral16     goldenSpiral_passes_conformal      Semantics.HCMMR.Law15
  [OK] goldenSpiral16     goldenSpiral_gate_admits           Semantics.HCMMR.Law15
  [OK] shear16            shear_fails_kahler                 Semantics.HCMMR.Law15
  [OK] TreeEmbeds         embed_monotonic                    Semantics.TreeDIATKruskal
  [OK] Q0_2_codec         q0_2_roundtrip                     Semantics.BraidField
  [OK] Law17              collapse_residual_form             Semantics.HCMMR.Law17
  [OK] PI                 encode_decode_roundtrip            Semantics.BraidDiatCodec

PROOF_CANDIDATE  (3/4 passing)
  [OK] goldenContractionEnergyDecrease                       Semantics.PistSimulation
  [FAIL] corkscrew_roundtrip    -- theorem not yet stated    (TYPED_MODEL, see s9)
  [OK] TreeDIAT_Kruskal       wqo_certificate                Semantics.TreeDIATKruskal
  [OK] phiContractionLaw      contract_norm_law              Semantics.PistSimulation

TYPED_MODEL  (3/3 listed -- sound readings, not machine-checkable)
  [i] Cartan dictionary    -- s1 of this document
  [i] Sidon mirror         -- s3 of this document
  [i] Laplacian resolution -- s6 of this document

VOCABULARY LINT: 7 deprecated labels still in use across 12 files.
  [i] "Dynamic Integer-Address Transform" to DIAT        (4 occurrences)
  [i] "Frustration Aligned Memory Management" to FAMM   (3 occurrences)
  [i] "Perfectly Imperfect Square Theory" to PIST        (5 occurrences)

SUMMARY: 11/12 machine-checkable standards passing. 7 deprecated labels remain.

10.5 Deprecation workflow

When a label is superseded (as many in §4 already are):

1. Add an entry to the [deprecated.*] table in STANDARDS.toml with the replacement term and migration path.
2. The vocabulary linter flags all occurrences.
3. PRs that touch files with deprecated labels must resolve them (or file an issue for a follow-up pass).
4. After a grace period (30 days suggested), the CI gate G2 hard-fails on unremediated occurrences.

This ensures the vocabulary lock converges rather than drifting.

10.6 Relationship to the receipt protocol

The compliance structure and the receipt protocol serve complementary roles:

	Compliance structure	Receipt protocol
Scope	Vocabulary, evidence tiers, CI gates	Per-operation audit trail
Enforcement	Pre-commit + CI	Runtime verification
Granularity	Per standard / per module	Per operation / per transformation
Failure mode	PR blocked, lint warning	ADMIT / HOLD / QUARANTINE
Retroactive	Yes — can lint old code	No — receipts are generated at runtime
Formal basis	Lean theorems + #eval witnesses	Lean theorems + hash chains

A CORE_MODULE standard should have both a compliance check (passes G1) and a receipt theorem (the operation's roundtrip is proven). A TYPED_MODEL standard has the compliance check aspirational and the receipt theorem unstated. This is by design — the compliance structure tracks the gap.

---

Observerless Research Stack — Geometric Substance Canonical Reconciliation v1.1