The core module lean/FrcCore/Theme/Brackets.lean — the substrate from first principles, no Mathlib, no axioms; one of the core's 142 modules (the index); it rests on no other module: 1 theorems (31 definitions): 1 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.
1/-!2# FrcCore.Theme.Brackets — window fractions, their brackets and the chains (the yangmills theme's first file, 8 November 2026)34The arithmetic in which the chart's constants enter the core: a window fraction `a/b` (1:D8, `FRC.Shell.Frame.frac_window`) is a5pair of an integer and a positive natural; on every shell with `2|a|b < p` it is read as the residue `a·b⁻¹`, two such6fractions with equal residues are equal, and their order is the order of the cross-products. Every comparison here is a7comparison of cross-products in the integers. The file holds the fractions (`WF`), their brackets (`BR`), the artanh chain of8the logarithm with its geometric majorant (`atanhChain`, `atanhTail`, `lnBr`: `ln x = k ln 2 + ln r` for `x = 2^k r`,9`y = (r − 1)/(r + 1) ≤ 1/3`), the six-place bracket of `π` (`piBr`), the readings of the chains at stage `12`10(`chain_readings`), and power series with window-fraction coefficients (`wsMul`, `wsInv`). Split from `Theme/YangMills.lean`11on 8 November 2026 (the round-01 revision of 46-yangmills; T15's note), which imports it. No axioms; imports nothing.12-/1314namespace FRC.YangMills1516/-- The `k`-th entry of a list, or `d` past its end (`List.getD` carries `propext`; this does not). -/17
def nth {α : Type} (d : α) : List α → Nat → α18 | [], _ => d19 | x :: _, 0 => x20 | _ :: xs, n + 1 => nth d xs n2122/-! ## Window fractions and the chains of the logarithm2324A window fraction `a/b` (1:D8, `FRC.Shell.Frame.frac_window`) is a pair of an integer and a positive natural; on every shell25with `2|a|b < p` it is read as the residue `a·b⁻¹`, two such fractions with equal residues are equal, and their order is the26order of the cross-products. Every comparison below is a comparison of cross-products in the integers. -/2728/-- A window fraction: numerator and positive denominator. -/29abbrev WF := Int × Nat3031namespace WF3233def norm (x : WF) : WF :=34 let g := Nat.gcd x.1.natAbs x.235 if g ≤ 1 then x else (x.1 / (g : Int), x.2 / g)36def add (x y : WF) : WF := norm (x.1 * y.2 + y.1 * x.2, x.2 * y.2)37def mul (x y : WF) : WF := norm (x.1 * y.1, x.2 * y.2)38def neg (x : WF) : WF := (-x.1, x.2)39def sub (x y : WF) : WF := add x (neg y)40def ofNat (n : Nat) : WF := (n, 1)41def frac (a : Int) (b : Nat) : WF := norm (a, b)42/-- The reciprocal of a nonzero fraction. -/43def inv (x : WF) : WF := if x.1 < 0 then (-(x.2 : Int), x.1.natAbs) else ((x.2 : Int), x.1.natAbs)44def div (x y : WF) : WF := mul x (inv y)45def lt (x y : WF) : Bool := decide (x.1 * (y.2 : Int) < y.1 * (x.2 : Int))46def le (x y : WF) : Bool := decide (x.1 * (y.2 : Int) ≤ y.1 * (x.2 : Int))47def pow (x : WF) : Nat → WF48 | 0 => (1, 1)49 | n + 1 => mul (pow x n) x50def sumRange (f : Nat → WF) : Nat → WF51 | 0 => (0, 1)52 | n + 1 => add (sumRange f n) (f n)53def max (x y : WF) : WF := if lt x y then y else x54def min (x y : WF) : WF := if lt x y then x else y55end WF5657/-- A bracket `[lo, hi]` of window fractions. -/58abbrev BR := WF × WF5960namespace BR61def add (x y : BR) : BR := (WF.add x.1 y.1, WF.add x.2 y.2)62def sub (x y : BR) : BR := (WF.sub x.1 y.2, WF.sub x.2 y.1)63def smul (n : Nat) (x : BR) : BR := (WF.mul (WF.ofNat n) x.1, WF.mul (WF.ofNat n) x.2)64/-- The bracket lies strictly inside `(lo, hi)`. -/65def within (x : BR) (lo hi : WF) : Bool := WF.lt lo x.1 && WF.lt x.2 hi66end BR6768/-- The artanh chain at stage `n`: `2 Σ_{k<n} y^{2k+1}/(2k+1)`, the frame's reading of `ln((1 + y)/(1 − y))` — a69𝔽Q-native chain of geometric rate (13-epi's class of the Machin chain), its partial sums window fractions. -/70def atanhChain (y : WF) (n : Nat) : WF :=71 WF.mul (WF.ofNat 2) (WF.sumRange (fun k => WF.div (WF.pow y (2 * k + 1)) (WF.ofNat (2 * k + 1))) n)7273/-- The geometric majorant of the chain's remainder, `2 y^{2n+1} / ((2n + 1)(1 − y²))` for `0 ≤ y < 1`. -/74def atanhTail (y : WF) (n : Nat) : WF :=75 WF.div (WF.mul (WF.ofNat 2) (WF.pow y (2 * n + 1))) (WF.mul (WF.ofNat (2 * n + 1)) (WF.sub (WF.ofNat 1) (WF.mul y y)))7677/-- `x ≥ 1` written as `2^k · r` with `1 ≤ r < 2`: `(k, r)` (with the fuel `f`). -/78def reduce2 (x : WF) : Nat → Nat × WF79 | 0 => (0, x)80 | f + 1 => if WF.lt x (WF.ofNat 2) then (0, x) else let (k, r) := reduce2 (WF.div x (WF.ofNat 2)) f; (k + 1, r)8182/-- The bracket of `ln x` for a window fraction `x ≥ 1` at stage `n`: `x = 2^k r`, `ln x = k ln 2 + ln r`, each logarithm83read by the artanh chain at `y = (x − 1)/(x + 1) ≤ 1/3` with the chain's partial sum below and the sum plus the84majorant above. -/85def lnBr (x : WF) (n : Nat) : BR :=86 let y2 := WF.frac 1 387 let l2 : BR := (atanhChain y2 n, WF.add (atanhChain y2 n) (atanhTail y2 n))88 let (k, r) := reduce2 x 6489 let y := WF.div (WF.sub r (WF.ofNat 1)) (WF.add r (WF.ofNat 1))90 BR.add (BR.smul k l2) (atanhChain y n, WF.add (atanhChain y n) (atanhTail y n))9192/-- The six-place bracket of `π`, `3.141592 < π < 3.141593`: the chart's reading of the constant, the one Mathlib certifies93(`Real.pi_gt_d6`, `Real.pi_lt_d6`) and 13-epi's Machin bracket contains; as a bracket of window fractions. -/94def piBr : BR := (WF.frac 3141592 1000000, WF.frac 3141593 1000000)9596/-- The chains at stage `12`: `ln 2 ∈ (0.69314, 0.69315)`, `ln 3 ∈ (1.0986, 1.0987)`, `ln 5 ∈ (1.6094, 1.6095)`,97`π ∈ (3.14159, 3.14160)`. -/98
theorem chain_readings :99 BR.within (lnBr (WF.ofNat 2) 12) (WF.frac 69314 100000) (WF.frac 69315 100000) = true ∧100 BR.within (lnBr (WF.ofNat 3) 12) (WF.frac 10986 10000) (WF.frac 10987 10000) = true ∧101 BR.within (lnBr (WF.ofNat 5) 12) (WF.frac 16094 10000) (WF.frac 16095 10000) = true ∧102 BR.within piBr (WF.frac 314159 100000) (WF.frac 314160 100000) = true := by103 decide +kernel104105/-! ## Power series in window fractions -/106107def wsCoeff (a : List WF) (k : Nat) : WF := nth (0, 1) a k108109def wsMul (a b : List WF) (n : Nat) : List WF :=110 (List.range n).map fun k =>111 (List.range (k + 1)).foldl (fun s i => WF.add s (WF.mul (wsCoeff a i) (wsCoeff b (k - i)))) (0, 1)112113def wsInv (a : List WF) (a0inv : WF) : Nat → List WF114 | 0 => []115 | n + 1 =>116 let r := wsInv a a0inv n117 if n = 0 then [a0inv]118 else r ++ [WF.neg (WF.mul a0inv ((List.range n).foldl119 (fun s i => WF.add s (WF.mul (wsCoeff a (i + 1)) (wsCoeff r (n - 1 - i)))) (0, 1)))]120121def fact : Nat → Nat122 | 0 => 1123 | k + 1 => fact k * (k + 1)124125end FRC.YangMills126