The de-drift pass: SU7 + bridge + 25519 numbered (14.12-14.14); whole tree wired into the default build

Spec catch-up (docs/fdrs.md, 504 -> 523 items):
- 14.12 The SU7 network arc numbered: Defs 208-210, Thms 103-110, Prop 152
  (probe gate, three-clause complexStep, causal grading, per-edge balance,
  decidable couplability + witnesses, transported traps, the conditional Kahn
  diamond, factored liveness) - honest-scope ledger carried verbatim.
- 14.13 The Phase-8 concretization bridge: Thm 111, Def 211, Thm 112.
- 14.14 Application capstone, the Curve25519 digit ring: Def 212, Thms 113-115.
- 14.7 / 14.11 / end-status updated with dated status notes, no silent
  rewrites; Realizability aggregator docstring corrected to the Theorem 43
  erratum form. 04-network-config.md records the SU7.x -> item mapping,
  discharging its ledger item 4.
- 33 fdrs.md anchor docstrings bind items to their actual declarations
  (SU7, bridge, 25519, plus previously unanchored Phase-13/9/7 items).

Build wiring (56 excluded modules -> default target; 308/308 reachable):
- New aggregators Modes/SyntheticPlace.lean, Modes/Adelic.lean,
  Applications.lean; VariableRadix / Realizability / Integration /
  ArithmeticFunctions aggregators extended.
- Latent name collision fixed on first co-import: GroupGrading's witness
  decls (chainGraph, chainPotential, frustratedTriangle, ...) scoped into
  the GroupGrading sub-namespace; base names preserved by design (they
  mirror Grading.lean's rational witnesses).
- lake build green: 3752 jobs, 0 errors, 0 sorry warnings.

Tooling:
- fdrs-summary: loud staleness warning when the yaml cache predates any
  live source (the "authoritative" banner was cache-served).
- lean_scan: block-comment closers no longer scanned as code (kills the
  phantom doc-comment sorries); sorry check strips inline block comments
  and backtick spans; RE_DECL accepts attribute-prefixed declarations.
- fdrs_graph: dot labels escape double quotes (Theorem 79's title had
  silently broken phase-1/5/13/global graph rendering since June).

Prose: TESTING.md build/sorry claims corrected to current reality; README
gains the SU7-machine and Applications results, the Applications/ layout
entry, and the everything-in-default-build note.

Artifacts regenerated (fdrs-rebuild). Status: 523 items, 99.4% proven
(520/523; the only genuine gap is Theorem 50, never formalized; 2 known
scaffolds honestly flagged), 0 axioms, 0 sorries, 0 modules outside the
default build.

Author: Hdpbilly

FdrsFormal.lean

@@ -11,9 +11,11 @@ Formalization of the fdrs.md specification, organized by mathematical dependenci
 - **FunctionSpaces/**: Mixed-radix complexes (𝕋(V), projections P_L, details Δ_L)
 - **NumberTheory/**: Analytic number theory (Dirichlet, characters, factorization)
 - **Integration/**: Combined topology + ANT (dual filtrations, complexity bounds)
-- **Modes/**: Modes of application (VariableRadix, ContextDependent, ExtendedBase, BaseZeroSea)
+- **Modes/**: Modes of application (VariableRadix incl. the Phase-13 Gosper cluster,
+  ContextDependent, ExtendedBase, BaseZeroSea, Adelic, SyntheticPlace)
 - **Analysis/**: Digit-conditional signal analysis (imported transitively via Modes)
 - **Composition/**: Multi-timeline routing and composition
+- **Applications/**: Corpus theory applied to deployed systems (Field25519Carry)
 
 For live status (file/theorem counts, sorries, stubs) run
 `python3 scripts/fdrs-summary`; counts are intentionally not hard-coded here.
@@ -42,3 +44,6 @@ import FdrsFormal.Modes
 
 -- Composition layer (Phase 5) - NEW 2026-01-30
 import FdrsFormal.Composition
+
+-- Applications layer (fdrs.md §14.14) - NEW 2026-07-12
+import FdrsFormal.Applications

FdrsFormal/Applications.lean

@@ -0,0 +1,29 @@
+/-
+Copyright 2026 Hyphaeic SPC.
+
+Licensed under the Hyphaeic Public License, Version 1.0 (the
+"License"); you may not use this file except in compliance with
+the License. You may obtain a copy of the License at
+
+https://github.com/hyphaeic/hpl
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or
+implied. See the License for the specific language governing
+permissions and limitations under the License.
+
+# Applications Module
+
+Corpus theory applied to concrete external systems. Applications are
+instantiations, not new mathematics: each module proves that a deployed artifact's
+load-bearing invariants are instances of numbered corpus items.
+
+## Contents
+
+- **Field25519Carry**: the field GF(2^255 − 19) under Ed25519 as a variable-radix
+  digit ring — carry conservation (the ledger identity), wrap holonomy 19, and the
+  carry schedule that licenses lazy reduction (fdrs.md §14.14).
+-/
+
+import FdrsFormal.Applications.Field25519Carry

FdrsFormal/Applications/Field25519Carry.lean

@@ -69,7 +69,9 @@ def numDigits : ℕ := 10
 This is the `RadixLaw` of `Modes.VariableRadix`, instantiated. -/
 def radixBits (i : ℕ) : ℕ := if i % 2 = 0 then 26 else 25
 
-/-- ωᵢ, the radix at digit i. -/
+/-- ωᵢ, the radix at digit i.
+
+**fdrs.md**: Definition 212 (the 25519 digit ring) [§14.14 · Phase 14] -/
 def radix (i : ℕ) : ℕ := 2 ^ radixBits i
 
 /-- Wᵢ = ∏_{j<i} ωⱼ = 2^⌈25.5·i⌉, the weight of digit i. -/
@@ -100,7 +102,9 @@ def carryStep (d : ℕ → ℕ) (i : ℕ) : ℕ → ℕ := fun k =>
 between them: the surplus that leaves i arrives at i+1 with exactly the
 weight that keeps the sum invariant (Wᵢ₊₁ = Wᵢ · ωᵢ).
 
-This is the ledger identity `issued = consumed + pending` at one interface. -/
+This is the ledger identity `issued = consumed + pending` at one interface.
+
+**fdrs.md**: Theorem 113 (a carry is a value-preserving redistribution) [§14.14 · Phase 14] -/
 theorem carryStep_preserves_value (d : ℕ → ℕ) (i : ℕ) :
     (carryStep d i i) * 2 ^ weightBits i
       + (carryStep d i (i + 1)) * 2 ^ weightBits (i + 1)
@@ -137,7 +141,9 @@ digit 0, and the weight it lands with is W₁₀ = 2^255, which is ≡ 19 (mod p
 So one unit of surplus leaving digit 9 re-enters at digit 0 as exactly 19.
 
 This is the FDRS holonomy of going once around the digit ring, and it is the
-*only* place the modulus enters the arithmetic. -/
+*only* place the modulus enters the arithmetic.
+
+**fdrs.md**: Theorem 114 (the wrap has holonomy 19, not 1) [§14.14 · Phase 14] -/
 theorem wrap_holonomy : (2 : ℕ) ^ weightBits 10 % p = holonomy := by
   rw [weightBits_ten]
   unfold p holonomy
@@ -196,7 +202,9 @@ the settling carry hands at most 2^41 / 2^26 = 2^15 to digit 1:
     digit 1 < 2^25 + 2^15 < 2^26.  ∎
 
 Every digit is therefore < 2^26 — `B` holds, the ledger is empty, and the
-next multiply's accumulator bound is licensed again. -/
+next multiply's accumulator bound is licensed again.
+
+**fdrs.md**: Theorem 115 (the schedule restores the bound — lazy reduction licensed) [§14.14 · Phase 14] -/
 theorem schedule_restores_bound
     (d1 : ℕ)          -- digit 1 after the sweep: canonical
     (h1 : d1 < 2 ^ 25)

FdrsFormal/Integration.lean

@@ -26,10 +26,11 @@ FDRS modes with analytic number theory primitives.
 - **RuntimeAlgebra**: Runtime operator algebra ℜ_N
 - **DualFiltrations**: Additive and multiplicative filtration structures
 - **Complexity**: Complexity bounds for operations
+- **ThreeLineMediator**: The LSU mediator and coupled system (fdrs.md §13.1)
 
 ## References
 
-- fdrs.md, Phase 4 (Integration)
+- fdrs.md, Phase 4 (Integration), Phase 13 §13.1 (the fixed-radix baseline)
 -/
 
 import FdrsFormal.Integration.BlockMemory.Definition
@@ -39,3 +40,5 @@ import FdrsFormal.Integration.Programs.IntegerSemantics
 import FdrsFormal.Integration.RuntimeAlgebra.Definition
 import FdrsFormal.Integration.DualFiltrations.Definition
 import FdrsFormal.Integration.Complexity.Definition
+import FdrsFormal.Integration.ThreeLineMediator.Definition
+import FdrsFormal.Integration.ThreeLineMediator.CoupledSystem

FdrsFormal/Integration/ThreeLineMediator/Definition.lean

@@ -199,7 +199,9 @@ theorem projectB_combine (b₁ b₂ : RadixSeq) (a : CompletedSpace b₁)
   rw [Nat.add_mul_div_left _ _ (by linarith [b₁.ge_two i] : 0 < b₁ i),
       Nat.div_eq_of_lt (a i).isLt]; simp
 
-/-- Combining the projections of a mediator element recovers the original -/
+/-- Combining the projections of a mediator element recovers the original.
+
+**fdrs.md**: Proposition 144 (Mediator ≅ A × B: the round-trip identities) [§13.1.2 · Phase 13] -/
 theorem combine_project (b₁ b₂ : RadixSeq)
     (x : CompletedSpace (productRadix b₁ b₂)) :
     combine b₁ b₂ (projectA b₁ b₂ x) (projectB b₁ b₂ x) = x := by

FdrsFormal/Modes.lean

@@ -15,12 +15,14 @@ permissions and limitations under the License.
 
 # Modes Module
 
-This module aggregates the three generalization modes of FDRS.
+This module aggregates the generalization modes of FDRS and the satellite
+complexes built on them.
 
 ## Contents
 
-- **VariableRadix/** (Mode I): Prefix-pure radix laws ω: Σ* → ℕ≥2
-  - Theorems A-B (Canonical bijection, Realizability)
+- **VariableRadix/** (Mode I, Phases 5-6 + 13): Prefix-pure radix laws ω: Σ* → ℕ≥2
+  - Theorems A-B (Canonical bijection, Realizability — corrected Theorem 43)
+  - Phase 13: generated (continued-fraction) timelines and the Gosper engine cluster
 
 - **ContextDependent/** (Mode II): Context-dependent radix laws Ω: Σ* × C → ℕ≥2
   - Theorems E-F (Lazy-eager, Structure preservation)
@@ -31,13 +33,23 @@ This module aggregates the three generalization modes of FDRS.
 
 - **Analysis/DigitConditional/** (Phase 11): Digit-conditional signal analysis
 
+- **Adelic/**: Place engines, product formula (ℚˣ), gauge bound, rigidity,
+  the AdelicLaw interface, function-field keystone
+
+- **SyntheticPlace/** (Phase 14): Gauge keystone, coupling, certificates,
+  conservation + rigidity, network geometry, grading, the SU7 network machine,
+  and the Phase-8 concretization bridge
+
 ## References
 
-- fdrs.md, Phases 5-6 (Modes), Phase 10 (Base-Zero Sea), Phase 11 (Digit-Conditional)
+- fdrs.md, Phases 5-6 (Modes), Phase 10 (Base-Zero Sea), Phase 11
+  (Digit-Conditional), Phase 13 (Generated Timelines), Phase 14 (Synthetic Place)
 -/
 
 import FdrsFormal.Modes.VariableRadix.VariableRadix
 import FdrsFormal.Modes.ContextDependent.ContextDependent
 import FdrsFormal.Modes.ExtendedBase
 import FdrsFormal.Modes.BaseZeroSea
 import FdrsFormal.Analysis.DigitConditional
+import FdrsFormal.Modes.Adelic
+import FdrsFormal.Modes.SyntheticPlace

FdrsFormal/Modes/Adelic.lean

@@ -0,0 +1,43 @@
+/-
+Copyright 2026 Hyphaeic SPC.
+
+Licensed under the Hyphaeic Public License, Version 1.0 (the
+"License"); you may not use this file except in compliance with
+the License. You may obtain a copy of the License at
+
+https://github.com/hyphaeic/hpl
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or
+implied. See the License for the specific language governing
+permissions and limitations under the License.
+
+# Adelic Complex Module
+
+Aggregates the adelic machine: heterogeneous place engines (p-adic ledgers and
+certified emission traps) under one scheduler with proven confluence, the product
+formula on ℚˣ in exact arithmetic, the finite-precision gauge bound, the rigidity
+boundary (no synthetic places on ℚ), and the function-field keystone.
+
+## References
+
+- Design records: `docs/archive/adelic-machine/` (superseded), `docs/function-field/`
+- fdrs.md Phase 13 (the emission-certificate family; `padic_emit_traps` is the
+  congruence certificate cited by Theorem 100's four-certificate accounting)
+-/
+
+import FdrsFormal.Modes.Adelic.PlaceEngine
+import FdrsFormal.Modes.Adelic.PadicEmission
+import FdrsFormal.Modes.Adelic.PadicHomographic
+import FdrsFormal.Modes.Adelic.PadicEmitTraps
+import FdrsFormal.Modes.Adelic.PadicBihEmission
+import FdrsFormal.Modes.Adelic.ValuationStream
+import FdrsFormal.Modes.Adelic.Complex
+import FdrsFormal.Modes.Adelic.ProductFormula
+import FdrsFormal.Modes.Adelic.ProductFormulaRat
+import FdrsFormal.Modes.Adelic.GaugeBound
+import FdrsFormal.Modes.Adelic.DriverCorrect
+import FdrsFormal.Modes.Adelic.Rigidity
+import FdrsFormal.Modes.Adelic.AdelicInterface
+import FdrsFormal.Modes.Adelic.FunctionFieldDegree

FdrsFormal/Modes/ContextDependent/Evolution/Preservation.lean

@@ -45,6 +45,8 @@ open FdrsFormal.Modes.VariableRadix
 **Theorem 45**: Context-switching preserves SU.
 
 If a system has CSU, then every context visited in any trace satisfies SU.
+
+**fdrs.md**: Theorem 45 (Context-switching preserves SU) [§7.2.4 · Phase 7]
 -/
 theorem csu_preserved_along_trace {C E : Type*}
     [ContextSpace C] [InitialContext C] [EventSpace E]

FdrsFormal/Modes/ExtendedBase/CarryRouteUnification.lean

@@ -157,6 +157,8 @@ Odometer routing decision: given a carry event at position `pos`,
 determine whether to propagate (and to which position).
 
 Returns `true` (propagate to pos+1) iff the event is OVERFLOW.
+
+**fdrs.md**: Definition 149 (Carry-as-route) [§9.9.2 · Phase 9]
 -/
 def carryRouteDecision (ce : CarryEvent) : Bool :=
   match ce with
@@ -238,6 +240,8 @@ and consults `carryRouteDecision` to determine whether to propagate.
 
 This is operationally the event-driven perspective: each OVERFLOW
 event at position `pos` triggers an INJECT at position `pos+1`.
+
+**fdrs.md**: Definition 150 (Unified spatial tick) [§9.9.3 · Phase 9]
 -/
 def unifiedSpatialTick {k : ℕ} (M : Fin k → ℕ) (b : Fin k → ℕ)
     (hb : ∀ i, 1 ≤ b i) (hbM : ∀ i, b i ≤ M i)

FdrsFormal/Modes/SyntheticPlace.lean

@@ -0,0 +1,67 @@
+/-
+Copyright 2026 Hyphaeic SPC.
+
+Licensed under the Hyphaeic Public License, Version 1.0 (the
+"License"); you may not use this file except in compliance with
+the License. You may obtain a copy of the License at
+
+https://github.com/hyphaeic/hpl
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or
+implied. See the License for the specific language governing
+permissions and limitations under the License.
+
+# Synthetic Place Complex Module (Phase 14)
+
+Aggregates the synthetic place complex: the gauge keystone (SU0), coupling and the
+ragged regime (SU1), the admissibility trap (SU2), zoom-out restriction (SU3),
+conservation / interface balance / rigidity (SU4), network geometry (SU5), the
+digit-coupling axes — grading, currencies, windows, nested charts, the non-abelian
+arc (SU6), and the SU7 network machine (`Config` + `complexStep`: balance,
+couplability, traps, determinacy, liveness) with the Phase-8 concretization bridge.
+
+## References
+
+- fdrs.md Phase 14 (Definitions 192–211, Theorems 83–112, Propositions 147–152)
+- Design records: `docs/synthetic-place/00-thesis.md` … `04-network-config.md`
+-/
+
+-- SU0–SU5: the statics
+import FdrsFormal.Modes.SyntheticPlace.GaugeUltrametric
+import FdrsFormal.Modes.SyntheticPlace.Composition
+import FdrsFormal.Modes.SyntheticPlace.AdmissibilityTrap
+import FdrsFormal.Modes.SyntheticPlace.Restriction
+import FdrsFormal.Modes.SyntheticPlace.Conservation
+import FdrsFormal.Modes.SyntheticPlace.InterfaceBalance
+import FdrsFormal.Modes.SyntheticPlace.ConservationRigidity
+import FdrsFormal.Modes.SyntheticPlace.TraceGeometry
+import FdrsFormal.Modes.SyntheticPlace.NetworkGauge
+
+-- SU6: digit coupling — grading, currencies, windows, nested charts
+import FdrsFormal.Modes.SyntheticPlace.Grading
+import FdrsFormal.Modes.SyntheticPlace.CurrencyBalance
+import FdrsFormal.Modes.SyntheticPlace.WindowAccountability
+import FdrsFormal.Modes.SyntheticPlace.WindowBoundary
+import FdrsFormal.Modes.SyntheticPlace.NestedChain
+import FdrsFormal.Modes.SyntheticPlace.NestedDilation
+
+-- SU6′: the non-abelian arc
+import FdrsFormal.Modes.SyntheticPlace.GroupGrading
+import FdrsFormal.Modes.SyntheticPlace.CircleEmit
+import FdrsFormal.Modes.SyntheticPlace.SE2Pose
+import FdrsFormal.Modes.SyntheticPlace.SE2Engine
+import FdrsFormal.Modes.SyntheticPlace.SE2Tight
+
+-- SU7: the network machine (§14.12)
+import FdrsFormal.Modes.SyntheticPlace.NetworkConfig
+import FdrsFormal.Modes.SyntheticPlace.NetworkComplexStep
+import FdrsFormal.Modes.SyntheticPlace.NetworkBalance
+import FdrsFormal.Modes.SyntheticPlace.NetworkCouplability
+import FdrsFormal.Modes.SyntheticPlace.NetworkTraps
+import FdrsFormal.Modes.SyntheticPlace.NetworkDeterminacy
+import FdrsFormal.Modes.SyntheticPlace.NetworkLiveness
+
+-- The Phase-8 concretization bridge (§14.13)
+import FdrsFormal.Modes.SyntheticPlace.NetworkBridge