The core module lean/FrcCore/Keys/Relaxation.lean — the substrate from first principles, no Mathlib, no axioms; one of the core's 137 modules (the index); it rests on 19 modules: Nat, Pigeonhole, Shell, Series, Cycle, Ring, FrameCore, Frame, Theme/Quadratic, Theme/Field, Theme/Symbol, Theme/Gravity, Theme/Shift, Theme/Lattice, Theme/Drift, Theme/Relaxation, Theme/Window, Theme/Static, Poly: 14 theorems (0 definitions): 14 with no axioms, 0 at tier 1 (propext, Quot.sound), 0 at tier 2 (Classical.choice), 0 red; the mark's colour is the library's (green, the core; red a proof the gate rejects), each declaration's axioms on hover; the small plain glyph marks a definition (no proof, no axioms; on the ledger pages the plain glyph is instead a module cited as a whole). Each declaration is anchored; the ledger predicates cite them by name. ▶ open in Lean Live · axioms.log.
1import FrcCore.Theme.Symbol2import FrcCore.Theme.Lattice3import FrcCore.Theme.Drift4import FrcCore.Theme.Relaxation5import FrcCore.Theme.Window6import FrcCore.Theme.Static78/-!9# FrcCore.Keys.Relaxation — the keyed theorems of the relaxation theme (ledger migration, task LM19)1011One declaration per key, `FRC.Ledger.p<key>`, generated by `make_keys.py` from the ledgers' Lean bindings: the theorem12that every row carrying the key asserts, proved from the themes alone. The paper's module keeps its declaration13`FRC.<Module>.p<key>` as an alias. Every declaration has no axioms (`check_core_axioms.py`).14-/1516namespace FRC.Ledger1718-- Keys of the relaxation theme (generated by make_keys.py from the ledgers' Lean bindings; edit the ledgers, not this file)19/-- p21006 — 21:C26. The Kuramoto form is the chart of C22: on every shell the pair-tally current $z-z^{-1}$ is the centred drive-difference of the tally, $W(zg)-W(zg^{-1})=(g-g^{-1})(z-z^{-1})$, the failure tally is the mismatch norm $(1-z)(1-z^{-1})$, and an odd adjacency-local kernel is a multiple of the central difference; $\sin(\theta_y-\theta_x)$ is the chart of $(z-z^{-1})/2i$. -/20
theorem p21006 : (∀ {p : Nat} [FRC.Pos p] (z w g h : FRC.Shell p), FRC.Relaxation.tally (z * g) (w * h) + -FRC.Relaxation.tally (z * h) (w * g) = (g + -h) * FRC.Relaxation.current z w) ∧ (∀ {p : Nat} [FRC.Pos p] (z w : FRC.Shell p), z * w = (1 : FRC.Shell p) → ((1 : FRC.Shell p) + -z) * ((1 : FRC.Shell p) + -w) = FRC.Relaxation.failure z w) ∧ ∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ (n : Nat) {a b c : FRC.Shell p}, FRC.Relaxation.Odd a b c → ∀ (f : Nat → FRC.Shell p) (i : Nat), FRC.Relaxation.kernel n a b c f i = a * FRC.Lattice.cdiff n f i :=21 And.intro @FRC.Relaxation.tally_gradient (And.intro @FRC.Relaxation.failure_norm (@FRC.Relaxation.odd_kernel_is_cdiff))22/-- p21016 — 21:C1. The linearised dynamics is the gradient flow of a coherence free energy --- its current derived from the pair tally conditional on channel unity (Lemma~\ref{lem:pairtally}) --- and a locked cluster of $m$ unit-winding cells couples with coefficient exactly $m$. -/23theorem p21016 : (∀ {p : Nat} [FRC.Pos p] (z : FRC.Shell p) (m : Nat), FRC.Shell.sumRange (fun x => z) m = FRC.Shell.ofNat m * z) ∧ (∀ {p : Nat} [FRC.Pos p] (z w : FRC.Shell p), z * w = (1 : FRC.Shell p) → (z + -w) * (z + -w) = -(((1 : FRC.Shell p) + (1 : FRC.Shell p) + -z + -w) * ((1 : FRC.Shell p) + (1 : FRC.Shell p) + z + w))) ∧ (∀ {p : Nat} [FRC.Pos p] (z w g h : FRC.Shell p), FRC.Relaxation.tally (z * g) (w * h) + -FRC.Relaxation.tally (z * h) (w * g) = (g + -h) * FRC.Relaxation.current z w) ∧ ∀ {p : Nat} [FRC.Pos p] (n : Nat), (0 : Nat) < n → ∀ (f : Nat → FRC.Shell p), FRC.Shell.sumRange (fun i => FRC.Lattice.fdiff n f i * FRC.Lattice.fdiff n f i) n = -FRC.Shell.sumRange (fun i => FRC.Cycle.cyc n f i * FRC.Lattice.lap n f i) n :=24 And.intro @FRC.Drift.locked_sum (And.intro @FRC.Drift.pair_tally (And.intro @FRC.Relaxation.tally_gradient (@FRC.Relaxation.leakage_contraction)))25/-- p21019 — 21:C4. The equivalence principle as an identity: the gravitational and the inertial coefficient are one cardinality, which cancels inside the two-shift law, $(m\,g)/m=g$; the bias field is clock rate, giving the redshift $\Delta f/f=Gm/rc^2$ [chart]; the turnaround radius against the Hubble drive [chart]. -/26theorem p21019 : ∀ (m g : Nat), (0 : Nat) < m → m * g / m = g :=27 @FRC.Relaxation.equivalence_cancel28/-- p21022 — 21:C7. Channel unity forces the spatial bias to equal the temporal one: the registered rate $M/B$ and the dwell per quantum are the two faces of one window count (the gaps of the Christoffel word take the two values $\lfloor B/M\rfloor$ and $\lceil B/M\rceil$), read as space and time through B4, so $\gamma=1$ [chart], restoring the full light deflection $4Gm/c^2b$ [chart]. -/29theorem p21022 : (∀ {p : Nat} [FRC.Pos p] {β γ : FRC.Shell p}, ((1 : FRC.Shell p) + (1 : FRC.Shell p)) * γ + -β = (1 : FRC.Shell p) → γ = (1 : FRC.Shell p) → β = (1 : FRC.Shell p)) ∧ (∀ {M : Nat → Nat} {B : Nat} (s : FRC.Relaxation.State) (k : Nat), s.acc + k * M s.mu < B → FRC.Relaxation.run M B k s = { mu := s.mu, acc := s.acc + k * M s.mu }) ∧ ∀ (M B c d : Nat), (0 : Nat) < M → c < M → c + d * M < B → B ≤ c + (d + (1 : Nat)) * M → B / M ≤ d + (1 : Nat) ∧ d + (1 : Nat) ≤ B / M + (1 : Nat) :=30 And.intro @FRC.Drift.cover_triangle (And.intro @FRC.Relaxation.quiet_run (@FRC.Relaxation.dwell_two_values))31/-- p21024 — 21:C9. The discrete Fierz--Pauli functional, exactly gauge-invariant and the unique adjacency-local stiffness on the shell (the spin-one case is unique-Maxwell). -/32theorem p21024 : (∀ {p : Nat} [FRC.Pos p] (n : Nat), (0 : Nat) < n → ∀ (f g : Nat → FRC.Shell p), FRC.Shell.sumRange (fun i => FRC.Lattice.cdiff n f i * FRC.Cycle.cyc n g i) n = -FRC.Shell.sumRange (fun i => FRC.Cycle.cyc n f i * FRC.Lattice.cdiff n g i) n) ∧ (∀ {p : Nat} [FRC.Pos p] (n : Nat), (0 : Nat) < n → ∀ (f g : Nat → FRC.Shell p), FRC.Shell.sumRange (fun i => FRC.Lattice.fdiff n f i * FRC.Cycle.cyc n g i) n = -FRC.Shell.sumRange (fun i => FRC.Cycle.cyc n f i * FRC.Lattice.bdiff n g i) n) ∧ (∀ {p : Nat} [FRC.Pos p] (η : Nat → FRC.Shell p) {n : Nat} {w₀ w₁ t : FRC.Shell p}, (1 : Nat) < n → η (0 : Nat) * w₀ = (1 : FRC.Shell p) → η (1 : Nat) * w₁ = (1 : FRC.Shell p) → ((1 : FRC.Shell p) + (1 : FRC.Shell p)) * t = (1 : FRC.Shell p) → ∀ (a₁ a₂ a₃ a₄ : FRC.Shell p), (∀ (k ξ : Nat → FRC.Shell p) (h : Nat → Nat → FRC.Shell p), (∀ (μ ν : Nat), h μ ν = h ν μ) → FRC.Symbol.tensForm η n a₁ a₂ a₃ a₄ k (FRC.Symbol.gauge h k ξ) = FRC.Symbol.tensForm η n a₁ a₂ a₃ a₄ k h) ↔ ∃ c, a₁ = -c ∧ a₂ = ((1 : FRC.Shell p) + (1 : FRC.Shell p)) * c ∧ a₃ = -(((1 : FRC.Shell p) + (1 : FRC.Shell p)) * c) ∧ a₄ = c) ∧ (∀ {p : Nat} [FRC.Pos p] (η : Nat → FRC.Shell p) (n : Nat) (c : FRC.Shell p) (k ξ : Nat → FRC.Shell p) {h : Nat → Nat → FRC.Shell p}, (∀ (μ ν : Nat), h μ ν = h ν μ) → FRC.Symbol.tensForm η n (-c) (((1 : FRC.Shell p) + (1 : FRC.Shell p)) * c) (-(((1 : FRC.Shell p) + (1 : FRC.Shell p)) * c)) c k (FRC.Symbol.gauge h k ξ) = FRC.Symbol.tensForm η n (-c) (((1 : FRC.Shell p) + (1 : FRC.Shell p)) * c) (-(((1 : FRC.Shell p) + (1 : FRC.Shell p)) * c)) c k h) ∧ (∀ {p : Nat} [FRC.Pos p] (η : Nat → FRC.Shell p) {n : Nat} {w : FRC.Shell p}, (0 : Nat) < n → η (0 : Nat) * w = (1 : FRC.Shell p) → ∀ (a₁ a₂ : FRC.Shell p), (∀ (k A : Nat → FRC.Shell p) (z : FRC.Shell p), FRC.Symbol.vecForm η n a₁ a₂ k (FRC.Symbol.shift A k z) = FRC.Symbol.vecForm η n a₁ a₂ k A) ↔ a₁ + a₂ = (0 : FRC.Shell p)) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ (n : Nat) {a b c : FRC.Shell p}, FRC.Relaxation.Odd a b c → ∀ (f : Nat → FRC.Shell p) (i : Nat), FRC.Relaxation.kernel n a b c f i = a * FRC.Lattice.cdiff n f i) ∧ ∀ {p : Nat} [FRC.Pos p] (n : Nat), (0 : Nat) < n → ∀ (f : Nat → FRC.Shell p) (i : Nat), FRC.Lattice.bdiff n (FRC.Lattice.fdiff n f) i = FRC.Lattice.lap n f i :=33 And.intro @FRC.Lattice.central_difference_adjoint (And.intro @FRC.Lattice.forward_difference_adjoint (And.intro @FRC.Symbol.fierz_pauli_unique (And.intro @FRC.Symbol.fierz_pauli_invariant (And.intro @FRC.Symbol.maxwell_unique (And.intro @FRC.Relaxation.odd_kernel_is_cdiff (@FRC.Relaxation.bdiff_fdiff))))))34/-- p21026 — 21:C11. The nonlinear completion forced: the exact cut-flux law (transfer antisymmetry) and the winding grading (sectors multiply, an equivariant operation preserves the grade, an invariant configuration in a nonzero winding sector vanishes) forbid independent static self-sourcing, the clock-comparison cocycle makes the exponential reading unique (exactly the character $\gen^{-\Delta n}$, $e^{-u}$ its observer lift), and Deser's bootstrap does not apply because what gravitates is winding rate. -/35theorem p21026 : (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ (n : Nat) (J : Nat → Nat → FRC.Shell p), (∀ (x y : Nat), J x y = -J y x) → ∀ (R : Nat → Bool), FRC.Shell.sumRange (fun x => FRC.Drift.ind R x * FRC.Shell.sumRange (fun y => J x y) n) n = FRC.Shell.sumRange (fun x => FRC.Drift.ind R x * FRC.Shell.sumRange (fun y => ((1 : FRC.Shell p) + -FRC.Drift.ind R y) * J x y) n) n) ∧ (∀ {p : Nat} [FRC.Pos p] (g : FRC.Shell p) (a b : Nat), g ^ (a + b) = g ^ a * g ^ b) ∧ (∀ {p : Nat} [FRC.Pos p] (f : Nat → FRC.Shell p), f (0 : Nat) = (1 : FRC.Shell p) → (∀ (a b : Nat), f (a + b) = f a * f b) → ∀ (a : Nat), f a = f (1 : Nat) ^ a) ∧ (∀ {p : Nat} [FRC.Pos p] (g : FRC.Shell p) {a b : Nat} {f h : Nat → FRC.Shell p}, FRC.Static.Graded g a f → FRC.Static.Graded g b h → FRC.Static.Graded g (a + b) fun x => f x * h x) ∧ (∀ {p : Nat} [FRC.Pos p] (g : FRC.Shell p) (k : Nat) (T : (Nat → FRC.Shell p) → Nat → FRC.Shell p), (∀ (f : Nat → FRC.Shell p) (x : Nat), T f (x + (1 : Nat)) = T (fun y => f (y + (1 : Nat))) x) → (∀ (c : FRC.Shell p) (f f' : Nat → FRC.Shell p), (∀ (y : Nat), f' y = c * f y) → ∀ (x : Nat), T f' x = c * T f x) → ∀ {f : Nat → FRC.Shell p}, FRC.Static.Graded g k f → FRC.Static.Graded g k (T f)) ∧ ∀ {p : Nat} [FRC.Pos p], FRC.Nat.isPrime p → ∀ (g : FRC.Shell p) (m : Nat), g ^ m ≠ (1 : FRC.Shell p) → ∀ {f : Nat → FRC.Shell p}, FRC.Static.Graded g (0 : Nat) f → FRC.Static.Graded g m f → ∀ (x : Nat), f x = (0 : FRC.Shell p) :=36 And.intro @FRC.Drift.gauss_law (And.intro @FRC.Drift.character_composition (And.intro @FRC.Drift.character_unique (And.intro @FRC.Static.graded_mul (And.intro @FRC.Static.equivariant_graded (@FRC.Static.selection)))))37/-- p21027 — 21:C12. The exact static profile in cut form: on an equitable radial partition a static locked exterior exists exactly where the enclosed demand is within the capacity of every cut, $Q_r\le\varkappa A_r$ (the condition necessary on every chart), and ends at the first cut that fails, the slip core ($\sqrt{m/30}\le r_*\le\lceil\sqrt{m/12}\,\rceil$ on the graph balls at unit capacity, $r_*=\sqrt{Gm}$ in the isotropic chart with $4\pi r^{2}$ its [chart] reading); horizonless, operationally black at $r_f=r_s/\ln\Omega$ [chart]; the $r_f$-anchored claims stated in the substrate coordinate, $r_*<r_f<M$ for $M>(\ln\Omega/2)^{2}$ Planck masses. -/38theorem p21027 : (∀ (κ : Nat) (A Q : Nat → Nat), (∃ t, FRC.Static.Static κ A Q t) ↔ ∀ (r : Nat), Q r ≤ κ * A r) ∧ (∀ (κ : Nat) (A Q : Nat → Nat) (r : Nat), κ * A r < Q r → ¬∃ t, FRC.Static.Static κ A Q t) ∧ (∀ (κ m r : Nat), m ≤ (12 : Nat) * κ * (r * r) → m ≤ κ * FRC.Static.cutArea r) ∧ (∀ (κ m r : Nat), (1 : Nat) ≤ r → (30 : Nat) * κ * (r * r) < m → κ * FRC.Static.cutArea r < m) ∧ ((10000 : Nat) ≤ (1 : Nat) * FRC.Static.cutArea (29 : Nat) ∧ (1 : Nat) * FRC.Static.cutArea (28 : Nat) < (10000 : Nat)) ∧ ∀ (L M : Nat), L * L < (4 : Nat) * M → (2 : Nat) < L → (0 : Nat) < M → L * L * M < (2 : Nat) * M * ((2 : Nat) * M) ∧ (2 : Nat) * M < L * M :=39 And.intro @FRC.Static.static_iff (And.intro @FRC.Static.slip_of_exceeds (And.intro @FRC.Static.exterior_of_sq (And.intro @FRC.Static.slip_of_sq (And.intro @FRC.Static.slip_instance (@FRC.Drift.cut_ordering)))))40/-- p21036 — 21:C21. The defect chain: relative-cycle defect with exact recurrence; the compression identity (relaxation $=$ unresolved leakage, recurrence retained), the leakage over a window counted as the chronons at which the registered outcome fails to close; the pair-tally current (the current $z-z^{-1}$ derived, the sine its chart, conditional on channel unity); binding bookkeeping decided --- substrate winding sources the field, the defect registered-side, $\eta_{\mathrm{Nordtvedt}}=0$ on that bookkeeping, the three coefficients of a bound composite not derived separately. -/41theorem p21036 : (∀ (L a t : Nat), (0 : Nat) < L → (t * a % L = (0 : Nat) ↔ FRC.Drift.firstReturn L a ∣ t)) ∧ ((420 / 28 : Nat) = (15 : Nat) ∧ (420 / 60 : Nat) = (7 : Nat) ∧ (420 : Nat) % (28 : Nat) = (0 : Nat) ∧ (420 : Nat) % (60 : Nat) = (0 : Nat) ∧ (60 : Nat) % (4 : Nat) = (0 : Nat) ∧ (28 : Nat) % (4 : Nat) = (0 : Nat) ∧ ((15 : Nat) - (7 : Nat)) % (420 : Nat) = (8 : Nat) ∧ FRC.Drift.firstReturn (105 : Nat) (8 : Nat) = (105 : Nat) ∧ FRC.Drift.firstReturn (420 : Nat) (8 : Nat) = (105 : Nat)) ∧ (∀ {p : Nat} [FRC.Pos p] (z w : FRC.Shell p), z * w = (1 : FRC.Shell p) → (z + -w) * (z + -w) = -(((1 : FRC.Shell p) + (1 : FRC.Shell p) + -z + -w) * ((1 : FRC.Shell p) + (1 : FRC.Shell p) + z + w))) ∧ (∀ {p : Nat} [FRC.Pos p] (n : Nat), (0 : Nat) < n → ∀ (P f : Nat → FRC.Shell p), (∀ (x : Nat), P x * P x = P x) → FRC.Shell.sumRange (fun x => P x * (P ((x + (1 : Nat)) % n) * f ((x + (1 : Nat)) % n) * (P ((x + (1 : Nat)) % n) * f ((x + (1 : Nat)) % n)))) n + FRC.Shell.sumRange (fun x => ((1 : FRC.Shell p) + -P x) * (P ((x + (1 : Nat)) % n) * f ((x + (1 : Nat)) % n) * (P ((x + (1 : Nat)) % n) * f ((x + (1 : Nat)) % n)))) n = FRC.Shell.sumRange (fun x => P x * (f x * f x)) n) ∧ (∀ (L a T : Nat), FRC.Static.leakage L a T + FRC.Static.returns L a T = T) ∧ ∀ (L a T : Nat), (0 : Nat) < L → (1 : Nat) ≤ T → FRC.Static.leakage L a T = T - ((T - (1 : Nat)) / FRC.Drift.firstReturn L a + (1 : Nat)) :=42 And.intro @FRC.Drift.return_iff (And.intro @FRC.Drift.defect_instance (And.intro @FRC.Drift.pair_tally (And.intro @FRC.Drift.compression (And.intro @FRC.Static.leakage_add_returns (@FRC.Static.leakage_eq)))))43/-- p21037 — 21:C22. Induced relaxation: given the registered adjacency chart with unit capacity, the compressed evolution $K_{\mathrm S}=P_{\mathrm S}U_{\mathrm C}P_{\mathrm S}$ contracts by exactly the unresolved leakage, counted over a window as the chronons at which the registered outcome fails to close; the leading odd leakage kernel is forced to the central difference and the incidence composite is the Laplacian; the constitutive current is the pair-tally current, its window count the readout of the sine on the strata $C_8$, $C_{12}$; under the re-registration rule the mismatch reaches alignment in finitely many chronons --- the Kuramoto gradient flow its weak-defect, short-memory chart, sampled at the quantum. -/44theorem p21037 : (∀ {p : Nat} [FRC.Pos p] (n : Nat), (0 : Nat) < n → ∀ (P f : Nat → FRC.Shell p), (∀ (x : Nat), P x * P x = P x) → FRC.Shell.sumRange (fun x => P x * (P ((x + (1 : Nat)) % n) * f ((x + (1 : Nat)) % n) * (P ((x + (1 : Nat)) % n) * f ((x + (1 : Nat)) % n)))) n + FRC.Shell.sumRange (fun x => ((1 : FRC.Shell p) + -P x) * (P ((x + (1 : Nat)) % n) * f ((x + (1 : Nat)) % n) * (P ((x + (1 : Nat)) % n) * f ((x + (1 : Nat)) % n)))) n = FRC.Shell.sumRange (fun x => P x * (f x * f x)) n) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ (n : Nat) {a b c : FRC.Shell p}, FRC.Relaxation.Odd a b c → ∀ (f : Nat → FRC.Shell p) (i : Nat), FRC.Relaxation.kernel n a b c f i = a * FRC.Lattice.cdiff n f i) ∧ (∀ {p : Nat} [FRC.Pos p] (n : Nat), (0 : Nat) < n → ∀ (f : Nat → FRC.Shell p) (i : Nat), FRC.Lattice.bdiff n (FRC.Lattice.fdiff n f) i = FRC.Lattice.lap n f i) ∧ (∀ {p : Nat} [FRC.Pos p] (n : Nat), (0 : Nat) < n → ∀ (f : Nat → FRC.Shell p), FRC.Shell.sumRange (fun i => FRC.Lattice.fdiff n f i * FRC.Lattice.fdiff n f i) n = -FRC.Shell.sumRange (fun i => FRC.Cycle.cyc n f i * FRC.Lattice.lap n f i) n) ∧ ∀ {p : Nat} [FRC.Pos p] (z w g h : FRC.Shell p), FRC.Relaxation.tally (z * g) (w * h) + -FRC.Relaxation.tally (z * h) (w * g) = (g + -h) * FRC.Relaxation.current z w :=45 And.intro @FRC.Drift.compression (And.intro @FRC.Relaxation.odd_kernel_is_cdiff (And.intro @FRC.Relaxation.bdiff_fdiff (And.intro @FRC.Relaxation.leakage_contraction (@FRC.Relaxation.tally_gradient))))46/-- p21044 — 21:X4. \textbf{Misner's standing objection dissolves.} The exponential metric is derived, not posited as a self-coupled field equation, so the field-equation pathology Misner identified in exponential-metric gravity does not arise here. -/47theorem p21044 : (∀ {p : Nat} [FRC.Pos p], FRC.Nat.isPrime p → ∀ (g : FRC.Shell p) (m : Nat), g ^ m ≠ (1 : FRC.Shell p) → ∀ {f : Nat → FRC.Shell p}, FRC.Static.Graded g (0 : Nat) f → FRC.Static.Graded g m f → ∀ (x : Nat), f x = (0 : FRC.Shell p)) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ (n : Nat) (J : Nat → Nat → FRC.Shell p), (∀ (x y : Nat), J x y = -J y x) → ∀ (R : Nat → Bool), FRC.Shell.sumRange (fun x => FRC.Drift.ind R x * FRC.Shell.sumRange (fun y => J x y) n) n = FRC.Shell.sumRange (fun x => FRC.Drift.ind R x * FRC.Shell.sumRange (fun y => ((1 : FRC.Shell p) + -FRC.Drift.ind R y) * J x y) n) n) ∧ ∀ {p : Nat} [FRC.Pos p] (f : Nat → FRC.Shell p), f (0 : Nat) = (1 : FRC.Shell p) → (∀ (a b : Nat), f (a + b) = f a * f b) → ∀ (a : Nat), f a = f (1 : Nat) ^ a :=48 And.intro @FRC.Static.selection (And.intro @FRC.Drift.gauss_law (@FRC.Drift.character_unique))49/-- p21047 — 21:X7. \textbf{The equivalence principle} is an identity, not a postulate. -/50theorem p21047 : ∀ (m g : Nat), (0 : Nat) < m → m * g / m = g :=51 @FRC.Relaxation.equivalence_cancel52/-- p21066 — 21:C27. The pulse law of unit capacity: a transfer of $M\le N$ quanta over $N$ chronons is realised by the counts $s_k=\lfloor kM/N\rfloor$, which rise by at most one per chronon and reach $M$ at $k=N$ --- at most one quantum per chronon (Lemma~\ref{pre:unit}), the Christoffel word of Lemma~\ref{lem:isopair}, the sine its observer mean. -/53theorem p21066 : ∀ (N M : Nat), (0 : Nat) < N → M ≤ N → (∀ (k : Nat), ∃ s r, s * N + r = k * M ∧ r < N) ∧ (∀ (k s r s' r' : Nat), s * N + r = k * M → r < N → s' * N + r' = (k + (1 : Nat)) * M → r' < N → s ≤ s' ∧ s' ≤ s + (1 : Nat)) ∧ ∀ (s r : Nat), s * N + r = N * M → r < N → s = M :=54 @FRC.Relaxation.pulse_law55/-- p21067 — 21:C28. The registered relaxation terminates: under the re-registration rule, with a transfer per window at every mismatch at or below the start (the basin below the antipode, where the current vanishes), the mismatch of a link never grows, moves by at most one quantum per chronon, reaches exact alignment within $\sum_\mu\lceil B/M(\mu)\rceil$ chronons and stays there; the Kuramoto flow sampled at the quantum is its chart [chart]. -/56theorem p21067 : (∀ {M : Nat → Nat} {B : Nat}, (∀ (μ : Nat), M μ ≤ B) → M (0 : Nat) = (0 : Nat) → ∀ (k : Nat → Nat), (∀ (μ : Nat), (0 : Nat) < μ → B ≤ k μ * M μ) → ∀ (n : Nat) (s : FRC.Relaxation.State), s.mu ≤ n → s.acc < B → (FRC.Relaxation.run M B (FRC.Relaxation.budget k n) s).mu = (0 : Nat)) ∧ (∀ {M : Nat → Nat} {B : Nat}, (∀ (μ : Nat), M μ ≤ B) → M (0 : Nat) = (0 : Nat) → ∀ (k : Nat → Nat) (n : Nat), (∀ (μ : Nat), (0 : Nat) < μ → μ ≤ n → B ≤ k μ * M μ) → ∀ (s : FRC.Relaxation.State), s.mu ≤ n → s.acc < B → (FRC.Relaxation.run M B (FRC.Relaxation.budget k n) s).mu = (0 : Nat)) ∧ (∀ {M : Nat → Nat} {B : Nat}, (∀ (μ : Nat), M μ ≤ B) → ∀ {s : FRC.Relaxation.State}, (0 : Nat) < s.mu → s.acc < B → ∀ {k : Nat}, B ≤ k * M s.mu → (FRC.Relaxation.run M B k s).mu < s.mu) ∧ (∀ {M : Nat → Nat} {B : Nat}, M (0 : Nat) = (0 : Nat) → ∀ (t : Nat) {s : FRC.Relaxation.State}, s.acc < B → s.mu = (0 : Nat) → (FRC.Relaxation.run M B t s).mu = (0 : Nat)) ∧ (∀ {M : Nat → Nat} {B : Nat} (s : FRC.Relaxation.State), (FRC.Relaxation.step M B s).mu ≤ s.mu) ∧ ∀ {M : Nat → Nat} {B : Nat} (s : FRC.Relaxation.State), s.mu ≤ (FRC.Relaxation.step M B s).mu + (1 : Nat) :=57 And.intro @FRC.Relaxation.terminates (And.intro @FRC.Relaxation.terminates_basin (And.intro @FRC.Relaxation.drops_within (And.intro @FRC.Relaxation.run_aligned (And.intro @FRC.Relaxation.step_mu_le (@FRC.Relaxation.step_mu_ge)))))58/-- p21068 — 21:C29. The window count of the link's current is the readout of its quadratic weight, the sine its chart: on $C_8$ and $C_{12}$, the real-quadratic strata of the readout map, the current read at the worked scale counts the transfers per window within half a unit of $B\sin(2\pi\mu/N)$ [chart], and the readouts nest across scales. -/59theorem p21068 : (FRC.Relaxation.IsSqrt ((2 : Nat) * (3 : Nat) ^ (8 : Nat)) (114 : Nat) ∧ FRC.Relaxation.readoutNum (0 : Nat) (1 : Nat) (114 : Nat) (3 : Nat) (4 : Nat) = (114 : Nat) ∧ FRC.Relaxation.readoutDen (2 : Nat) (3 : Nat) (4 : Nat) = (162 : Nat) ∧ FRC.Relaxation.count (81 : Nat) (FRC.Relaxation.readoutNum (0 : Nat) (1 : Nat) (114 : Nat) (3 : Nat) (4 : Nat)) (FRC.Relaxation.readoutDen (2 : Nat) (3 : Nat) (4 : Nat)) = (57 : Nat) ∧ FRC.Relaxation.count (81 : Nat) (FRC.Relaxation.readoutNum (1 : Nat) (0 : Nat) (114 : Nat) (3 : Nat) (4 : Nat)) (FRC.Relaxation.readoutDen (1 : Nat) (3 : Nat) (4 : Nat)) = (81 : Nat)) ∧ (FRC.Relaxation.IsSqrt ((3 : Nat) * (3 : Nat) ^ (8 : Nat)) (140 : Nat) ∧ FRC.Relaxation.count (81 : Nat) (FRC.Relaxation.readoutNum (1 : Nat) (0 : Nat) (140 : Nat) (3 : Nat) (4 : Nat)) (FRC.Relaxation.readoutDen (2 : Nat) (3 : Nat) (4 : Nat)) = (41 : Nat) ∧ FRC.Relaxation.count (81 : Nat) (FRC.Relaxation.readoutNum (0 : Nat) (1 : Nat) (140 : Nat) (3 : Nat) (4 : Nat)) (FRC.Relaxation.readoutDen (2 : Nat) (3 : Nat) (4 : Nat)) = (70 : Nat) ∧ FRC.Relaxation.count (81 : Nat) (FRC.Relaxation.readoutNum (1 : Nat) (0 : Nat) (140 : Nat) (3 : Nat) (4 : Nat)) (FRC.Relaxation.readoutDen (1 : Nat) (3 : Nat) (4 : Nat)) = (81 : Nat)) ∧ (∀ {x s s' c : Nat}, (0 : Nat) < c → FRC.Relaxation.IsSqrt x s → FRC.Relaxation.IsSqrt (x * (c * c)) s' → s * c ≤ s' ∧ s' < (s + (1 : Nat)) * c) ∧ ∀ {x s s' : Nat}, FRC.Relaxation.IsSqrt x s → FRC.Relaxation.IsSqrt x s' → s = s' :=60 And.intro @FRC.Relaxation.readout_c8 (And.intro @FRC.Relaxation.readout_c12 (And.intro @FRC.Relaxation.isSqrt_nest (@FRC.Relaxation.isSqrt_unique)))61-- end keys6263end FRC.Ledger64