Repository navigation
Lean 4.35 / Mathlib v4.35.0 upgrade - #144
Merged
Merged
Conversation
Implements Tim's permanent release rule (2026-10-08, permanent 2026-10-30). check_release_ready.py gains a ledger leg: reads the main checkout's .claude-local/DEFECTS.md, applies its header's open-unit rule, fails on open content BEDROCK/BEDROCK-CANDIDATE and on untagged open units, fails with a distinct UNREADABLE status on a missing ledger, prints kind x severity counts, and adds --ledger-only and selftest controls. CLAUDE.md R-DEFECTS/R-RELEASE and tools/process/defect-ledger.md restated to the ruled rule. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Qj4hZFmT3jz71cMudY2wno
The badge sits with the other CI badges. The workflow's name, which GitHub uses as the badge label, now reads "Axiom Ledger (choice-free computability)", so it does not read as a check of T-SNAP or CLAIMS.md. A weekly schedule re-checks the ledger on main, since the path filters miss Kleene.lean and its imports. Editorial r2 PASS, adversary r2 PASS (two ordinary findings carried as outstanding); R-AR confirmed by Tim 2026-10-31. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Qj4hZFmT3jz71cMudY2wno
Rung B now requires one phrasing with formality "both" and states the measured 2026-10-31 formal coverage, so a formal null reads as bounded. New rung B2 searches Lean libraries: LeanExplore search_summary, then get_source_code on candidates, then GitHub code search language:Lean for the Reservoir long tail. tools/process/prior-art.md and CLAUDE.md R-PRIORART name the new ladder order (R-PRIORART line count unchanged). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Qj4hZFmT3jz71cMudY2wno
Gate round 1 fixes. Rung B rule 5 requires a "formal" phrasing ("both"
crowds Lean hits out of the capped list) and states coverage as a dated
sample, withdrawing the single-probe FLT miss. Rung B2 always runs,
records NOT RUN when LeanExplore is unavailable, credits LeanExplore,
and reads hypotheses off the elaborated type since source text can drop
section binders. Rung C, the null rule and the discovery line follow;
tools/process/prior-art.md renumbers to five rungs; CLAUDE.md says
"formal" (R-PRIORART line count unchanged).
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Qj4hZFmT3jz71cMudY2wno
Gate round 2 fixes. GitHub code search uses extension:lean (language:Lean returned 0 files where extension:lean returned 9). The elaborated type comes from #check only; get_dependencies returns names. paper_filter is restated to the tool schema. cam-combi dropped from the coverage sample. The null rule matches B2's NOT RUN scope. Rung C's trigger is reverted and the B2-citation rule deleted. prior-art.md mirrors these and names R-NOCONV's rung 5 explicitly; CLAUDE.md line count unchanged. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Qj4hZFmT3jz71cMudY2wno
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Qj4hZFmT3jz71cMudY2wno
First live run of the Lean-library rung (Kleene.lean, 2026-10-31) found the brief silent or wrong in several places; each change below was re-measured. - A tool present but refused by the permission mode is NOT RUN, never a null. - In-closure verification: scratch file, `lake env lean`, `#check` + `exact?`. - Out-of-closure declarations: PARTLY VERIFIED, source read, type not elaborated (Tim's ruling, 2026-10-31). - get_dependencies is a partial list returned as a JSON-encoded string; packages= filter; GitHub perPage and -repo: self-exclusion; LeanExplore index snapshot differs from the pinned Mathlib. - Caller pre-flight: coverage_gap is the owed list; find is a per-file lookup. - Lean-only citation form; paper_filter needs a full arXiv id; only a rate-limit 403/429 is a wait; theoremsearch `name` carries in-paper labels on arXiv hits but numbering is not unique. Gates: editorial, adversary, prior_art PASS at round 2 with ordinaries carried; copy_editor signed by Tim. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Qj4hZEe22hsY1FqfbKnnU2
DieCannotBe: loop/climb survey re-run and recorded verbatim; the ℕ∞ summary Statement names wiring one's c ≠ ⊤ and wiring two's join-free loop; "might fill both roles"; the no-switch underclaim replaced by an example (UpAndOver's die motion fires the corner, legs agree, oppose in neither order); a stronger no-corner CONTROL with OVER at a landing; Rocq Diaconescu.v pointer names the compatibility section; registration sentence rewrapped so "decided" attaches to UP-definedness; full path for LawvereTaboo; Harary-Palmer cited for the term only; ε₀ given both faces; "image motion" second sense dropped; t_snap_given_cover premise named; Rutten Cor 5.6 last clause split into its two halves; isolating test "exists"; toPart equation stated alone; Lemma 7.2 values as points of ℕ∞; 2-adic reversed doubling drops by exactly one (example). Die: bisimilar_equivalence and isBisim_preimage Readings; NO-GO Prop for 2 holds only classically; wlpo_of_isolating_infty names basic-discontinuity; isolating_infty_of_decEq docstring says "exists". ChoiceCannotBe: case 3 de Jong example pins Prop.instHeytingAlgebra (measured [propext] pinned, [propext, Quot.sound] unpinned); case 5 Rocq pointer names the compatibility section. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Qj4hZEe22hsY1FqfbKnnU2
DieCannotBe § I: loop/climb split adopts the stutter-step name (Sharma, arXiv:1210.0408, Def. 5, p. 4), read at the source; wiring two's loop owes nothing specific to the join, pointer names the right CONTROL; UpAndOver inhabitation pointer for the no-switch refutation. § XX: the exact-one equation states its ⊤ + 1 = ⊤ case at ℤ_[2]'s 0. Diaconescu.v current theorem uses pairs, not classes (both files). Die: t "satisfies" basic-discontinuity, "retrieved" restored. Rewrap of one orphan line. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Qj4hZEe22hsY1FqfbKnnU2
…ixes E17 (CARRYW4-C6-12, WLPDF-1, PFX-1): ZP-J Self-Reference v2.14, Wheel Addendum v1.9 (companion v1.7) and Keystone Addendum v1.27 now cite Lean files by full repository path. Rendered bare-basename count, pypdf: 0 in all four (was 30, 10, 2, 3). E20: RiemannSphere.lean UPDOWN-R3-1 a-j. The three-carrier 1/0 example is rebuilt over nonZeroDivisors, where 2/0 = 1/0 = wheelInf, with a trivial-submonoid control; wheelBot is placed as the answer to 0/0. New examples: Mathlib's inversion is not continuous at 0 of Q_2 (pointer to NormedField.continuousAt_inv); reachability against the ValuationRing.ValueGroup order (opposite to Mathlib's, same as Stacks 00ID); the reversed sNorm preorder is not antisymmetric. Ceiling/floor proofs use Rat.ceil_intCast_div_natCast and Rat.floor_intCast_div_natCast. WheelFrac.md WHEELFRAC-OUT 1-7: ring case of Carlstrom's semiring generality; common meadows not the only non-involutive kind (1406.2092 p. 2); bibliographic record and edition caveat for the locators; count dropped from the adjacency header; section VIII pointer; porthole and wall-taxonomy pointers; the meadow disclaimer's reason now rests on the reverse-leg example. WheelFrac.lean: wheelFork_not_collapsed docstring scoped, with inhabited-type and empty-type examples. Gates: two rounds; editorial, adversary, prior_art and the three-reader copy_editor panel PASS at round 2 with ordinary findings outstanding. Wheel.lean: [Set97] expanded (PA-W3), stale script line locator replaced by the PDF section (PA-W2). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Qj4hZEe22hsY1FqfbKnnU2
…on-0 link) Die.lean: wlpo_of_discrete_tag (Sec. XXIII); RosPart, toRos, toRos_surjective_iff (onto iff LPO), AllRosolini, rosIncl_surjective_iff and the EM/LPO pair (Sec. XXIII); wem_of_selectedTotal_propStep (Sec. VIII); em_of_trichotomy_propStep and trichotomy_of_em (Sec. IX). Each with PurityCheck entry and ssot.json row. DieCannotBe.lean: instances and controls as anonymous examples in Secs. X, XI, XXVII; the limit map NInf -> Ordinal (infinity to epsilon-zero, never to bottom of Ordinal) as one conditional example in Sec. XXVII, with epsilonZero's and fundamentalSeq's footprints printed; the Escardo-Knapp Sec. 2.8 Reading reworded now that toRos relates NInf to the Rosolini propositions. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Qj4hZEe22hsY1FqfbKnnU2
…prior-art) Bell 1993 via Baaz-Zach for the Prop-step selector; Kripke's schema (Knapp; TypeTopology SemiDecidable BKS+) for AllRosolini; TypeTopology disagreement-taboo' for wlpo_of_discrete_tag; the dropped isProp condition in RosPart; Escardo 2013 Sec. 11 quoted. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Qj4hZEe22hsY1FqfbKnnU2
Prior-art round 2: Baaz-Zach page is p. 14; "an instance of that result (Bell 1993 itself not retrieved)". Adversary round 1 (die landing): section X open question scoped to NInf, with two examples showing the Prop-step selector gives LPO on N and Option N; the limit-map example's (vi) is now DecidableEq Ordinal -> WLPO, with a classical CONTROL; "the limit map", NInf.infty named; Escardo section 11 reasons corrected and the quoted inference attributed to Escardo; Escardo-Knapp "correspond to". Lane C carry: section I's UpAndOver inhabitant at Type (HSet 2 dual, with an example), additive; the N-valued registration test landed in section IX with the Computable.const footprint printed and no statement footprint claimed; wlpo_of_isolating_infty docstring restores basic-discontinuity-taboo and the N-infinity-indexed WLPO and names Escardo's JSL paper; survey parenthetical dropped, Sharma marked a locator; touched lines re-flowed to 100. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Qj4hZEe22hsY1FqfbKnnU2
…V-1)
The limit-map conjunct (vi) holds with no L: a CONTROL now shows a
decidable equality on Ordinal.{0} gives weak excluded middle by deciding
the supremum over p of 1 against 0, and the Reading says so.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Qj4hZEe22hsY1FqfbKnnU2
…fixes Integrates lanes B3 (Loeb), A3 (E03-E05), L1 (choice/EM), L2b (order/valuation), L3b (ordinals), L4b (set theory), L5 (computability) and P3c (Path 3, ZP-E/C/H/M) onto illustrated 50ca261 as a single non-merge commit. gitRobot merge cannot target a worktree, so single-lane files were copied byte-for-byte from each lane tip (verified by diff against the lane commit) and the overlaps hand-merged: register.md and the README Framework table per row at the higher version; LEAN_CUSTOM_REGISTRY.md (A3 + B3 hunks); ChoiceCannotBe.lean (A3 hunk on the die-side text); scripts/build_zpm.py (P3c's R-M.1, A3's purity-box hunk; A3's AIT paragraph was deleted by P3c, so its re-wording has no site left). ssot.json regenerated from the SJV store; MANIFEST.md regenerated. Fixes ruled by Tim 2026-11-01: - ZP-M IV and companion 5: the code half is the computability fixed point (IsComputationalQuine), met by constant codes, not "weaker than a fixed point". - ZP-M R-M.1 and companion 6: the c0 / 0-of-Q2 correspondence map is "not located as of 2026-11-01", with the search recorded. - ZP-C intro and L-INF box: c0, bottom of MachinePhase, named; ZP-E I "from which" disambiguated. - Miniature.lean: time enters with the occurrence commitment (t_snap_given). - LawvereBridge.md, Incompleteness.md, SnapNucleus.md, Kruskal.md, Surprisal.md, ZeroParadox/README.md: wording per the ruling. Wall.md:19-20 held for Tim (unchanged from L4b). PDFs: ZP-M v1.17 (companion v1.12), ZP-C v1.32, ZP-E v3.68 rebuilt; other lanes' PDFs carried at their lane versions. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Qj4hZEe22hsY1FqfbKnnU2
Round-1 gate findings (all ORDINARY; copy-editor panel UNDECIDED on two MEANING votes) fixed on new bytes: - ZP-M R-M.1 and companion 6: the search record now says no single declared map sends c0 to 0, names all three files that mention both types, and names the undeclared composite (MachinePhase to Pole, then poleToSphere) that does. - ZP-M IV: a code with eval c = selfApply c; the predicate, not the code, is met by constant codes. - ZP-C: the remaining bare bottoms name their carrier. - Miniature.lean: KleeneStructure is a commitment the reading rests on, no class field; time enters with the occurrence commitment and CC-1. - Incompleteness.md cites Padic.valuation_zero; SnapNucleus.md says "statement"; Surprisal.md drops a count that goes stale. PDFs: ZP-M v1.18 (companion v1.13), ZP-C v1.33. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Qj4hZEe22hsY1FqfbKnnU2
…cope Both checkers skip vendored files by design (is_vendored: Vendored/ plus the backports in tools/verify/vendored_files.txt) and the pre-push hook reports them exempt, but the registry scope still counted them, so a push that changed a vendored header could never be satisfied. This mirrors the existing written exemption and adds none. Tim, 2026-11-01: "Narrow ledger scope". Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Qj4hZEe22hsY1FqfbKnnU2
The Quine atom is the die role SelfOnlyAt (a point stepping to itself and
to nothing else). New: zfset_selfOnlyAt_mem_iff (the role in ZFSet, with a
set stepping to its members, is exactly x = {x}) and
zfset_quine_role_unoccupied in Wall.lean; cofixSelf, dest_cofixSelf,
cofixSelf_selfOnlyAt and cofix_quine_role_occupied in Coalgebra.lean.
Wall.md's "identifying the two is a modelling commitment" is replaced by
the die statement with pointers and no cross-chart equation; the Coalgebra
FENCE keeps its wording and gains the die statement beside it.
DieCannotBe points at the named declarations instead of the anonymous
ZFSet example and adds the Unit always-true / empty-step control.
Ride-alongs: ChoicePurityInvariant.md "quotient-collapse"; Curry.md
attribution form and its floor-dual sentence pointed at the die role.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Qj4hZEe22hsY1FqfbKnnU2
…tions Adds cofix_subsingleton (Cofix idPF_Coalgebra.Obj has at most one point) and fences the coalgebra occupancy with it; scopes "each chart" to the two charts exhibited; names the referent of the ill-typed equation; fixes the extensionality direction and the reversed-orientation comment in Wall.lean; splits the DieCannotBe control into Statement and Reading; cites Aczel 1988 Ex. 1.3 and p. 13, Rutten 2000 Ex. 10.2(1), and points at the graph chart in HypersetOrder.lean. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Qj4hZEe22hsY1FqfbKnnU2
New ZeroParadox/Order/DieJoints.lean: cut points, joints and dual joints, the order-dual exchange, the bottom and well-order exclusions, the ends of ENNReal and ENat, order-reversing surjections, the 2-adic pole, and PinnedLimit giving a joint (NInf's infinity, epsilon-zero). Indexed in DieCannotBe sections I, XXVII and XXIX; registry entries for the three definitions; SSOT rows and MANIFEST synced. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Qj4hZEe22hsY1FqfbKnnU2
Land the canonical-cut examples (IsJoint at (Iio a, Ici a) iff Order.IsSuccLimit a, and the IsPredLimit mirror), with Mathlib pointers beside not_isJoint_of_isBot and isJoint_toDual_iff. Registry: dated search record for the arbitrary-pair form, no ruling or attribution in the public reasons. DieCannotBe: the end-as-cut-point Reading is conditional with named exclusions and a naming fence; pointers and the "at e0" scope fixed. Header, e0 example (now with epsilon0_ne_bot) and CONTROL label corrected. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Qj4hZEe22hsY1FqfbKnnU2
Ruling 149, the r9 copy-editor readers' verbatim fixes: the registry places IsDualJoint at (Set.Iic x, Set.Ioi x); the die index adds the linear-order premise to the successor-limit gloss and lists PinnedLimit occupants apart from the adjoined ends, with epsilon-zero named as neither end of Ordinal. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Qj4hZEe22hsY1FqfbKnnU2
With BotHasFirstStep L and 0 < p <= 1, trials p hp-almost every tape fires and gives snap_of_two_requirements' conclusion (snap_ae_of_firstStep), and is also Martin-Loef random (mlRandom_and_snap_ae). Hypotheses, neither discharged; almost every, not every (all-false tape control). Indexed in SnapCannotBe § II. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Qj4hZEe22hsY1FqfbKnnU2
…g fixes Ruling 152: cite Landsman, Typical = random, arXiv:2306.09226, section 4, p. 16 in mlRandom_and_snap_ae's Reading; "the examples below" becomes "the example below"; the CONTROL comment points "in" CrossingTrials section VIII rather than "closing" it. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Qj4hZEe22hsY1FqfbKnnU2
New experimental ZeroParadox/Information/MaxEntropy.lean: Shannon entropy on Fin n is at most log n with equality iff uniform; missing information log 2 - binEntropy p is zero iff p = 1/2; the maximizer is fairTape, and maxEntropy_mlRandom_and_snap_ae chains it to mlRandom_and_snap_ae; Kraft in measure form and ae_incompressible for any prefix-free decoder, with the appendFalse control. One SnapCannotBe index line; MANIFEST and ssot.json synced (34 rows). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Qj4hZEe22hsY1FqfbKnnU2
The header read "almost every fair-coin tape is incompressible for every prefix-free decoder" (almost every w, for all D), which is false: for every tape a prefix-free decoder on the words true^k ++ [false] compresses its prefixes without bound. ae_incompressible proves the other order (for all D, almost every w). Adversary round 13, D1 fix. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Qj4hZEe22hsY1FqfbKnnU2
Control gloss prices the witness subset; the max-entropy coin is one sufficient choice; missingInfo range scoped to 0 <= p <= 1; § IV Reading gets CARRIER plus Milovanov siblings and the Schnorr pointer; § V scopes Levin-Schnorr to uniform, Brudno to 0 < p < 1 in bits, and cites Hoyrup via Cenzer-Porter Thm 32 with the primary source; § I names Gibbs and PFR. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Qj4hZEe22hsY1FqfbKnnU2
Mechanical API fixes for v4.35.0 / Mathlib 56a00585 in NaturalOps, CorpusAudit/Relation and Order/Lattice. Axiom footprints of all declarations in the three modules unchanged against the v4.30.0-rc2 build. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Qj4hZEe22hsY1FqfbKnnU2
Move lean-toolchain to leanprover/lean4:v4.35.0 and re-pin Mathlib and its dependencies in lakefile.toml and lake-manifest.json. The rest of the upgrade series lands with it. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Qj4hZEe22hsY1FqfbKnnU2
CorpusAudit's Audit.lean and AuditChecks.lean now name v4.35.0 as the port target, and Audit.lean's change list records the Relation.lean kernelAccepts / addDeclCore maxRecDepth port fix. NaturalOps' provenance line says proof bodies were adjusted only for upstream API changes, each marked [ZP port]. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Qj4hZEe22hsY1FqfbKnnU2
Mathlib's Fintype deriving handler fails on v4.35 (its rw on Finset.mem_mk no longer matches under the stricter defeq transparency). Surprisal, Padic and Miniature scope backward.isDefEq.respectTransparency false to the one deriving inductive each, marked [ZP port]. Axiom footprints of every declaration in the three modules unchanged against the v4.30.0-rc2 build. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Qj4hZEe22hsY1FqfbKnnU2
…-free footprints Mathlib's WithTop.le_def/lt_def are now proved by grind, which brings in Classical.choice, and Set's strict subset now elaborates through the CompleteAtomicBooleanAlgebra order, which does too. Scoped instance selection restores the old footprints with names and statements unchanged: PricedInterface pins the bare WithTop.instLE/instLT, Snap routes the subset through Set.instDistribLattice. CategoricalBridge and Snap take the zero_le (a := _) fix. Four PricedInterface declarations now measure [propext], smaller than before (Tim, ruling 163). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Qj4hZEe22hsY1FqfbKnnU2
Proof bodies follow upstream API changes (rulings 157-191). New choice-free WithTop/WithBot order instances (ChoiceFreeWithTop.lean), psListMem and fairCoinFin2 restore footprints Mathlib 4.35 would have grown. Statement-level changes, each ruled: KleeneChoiceFree states core's now-private Nat.sqrt.iter types; Settheory/Model uses MinTropical; OrdinalChoiceEssential declares WellFounded instances; BottomInvariant's markov_sameShape names fairCoinFin2; DieNucleus prints Prop.completeLinearOrder. AxiomLedger rows updated (rulings 181-184). ssot.json gains the 10 new rows. No declaration gained Classical.choice; boddNat_eq gained propext and Quot.sound (accepted, ruling 181). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Qj4hZEe22hsY1FqfbKnnU2
At 4.35 its auto-generated name equals the one the Fact (Nat.Prime 2) instances in P8, InvTowerNorm, PolarityFlip and ValuationAFA_Padic get, so importing the whole corpus failed (footprints.py --build). Named, the whole-corpus import elaborates: 5164 declarations across 247 modules, 8/8 footprint controls match. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Qj4hZEe22hsY1FqfbKnnU2
BrudnoBridge.lean: Milovanov's kolmogorov-complexity-lean (Apache-2.0, Lake
dependency pinned at 7e711168) bridged to trials/MLRandom; the two test
definitions coincide at every measure; Brudno and Levin-Schnorr restated.
SnapEpsilonZero.lean: snap_of_firstStep_MLRandom instantiated as the corner
on WithBot Ordinal and the cover on {0} with the fixed points of omega-power,
related by an order isomorphism; snap_epsilon0_two_faces (rulings 195-202).
DieCannotBe XXIII states the carrier-to-run bridge, one way.
Stale prose corrected to 4.35 measurements; ChoiceCannotBe gains the
instance-relative statement-carried entry (ruling 192). Engineer's Takes
are Tim's (rulings 194, 202). CLAIMS.md and README.md held for editorial
review.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Qj4hZEe22hsY1FqfbKnnU2
…self-copy A full-corpus footprint diff against a complete 4.30 harvest found 16 declarations that gained Classical.choice. Restored: EmbedsInThreeRegularTree (psListMem), instZPSemilatticeEnd/instAbstractSelfAppEnd (hand-built Fin max; core's new Fin.instMax carries choice), IgnoranceSeam's streamBits/affineExt family (decide in place of == on Int; core's Int order package carries choice). no_selfCopyRef_of_fintype stays statement-carried through Mathlib's Fintype; no_selfCopyRef_of_finite_constructive proves the [Finite] form choice-free (ruling 210). APG.lean: decoration_unique_of_val proves decoration uniqueness for any quiver at [propext, Quot.sound], by induction on the target's rank (Aczel's AFA2), with a [Finite V] corollary (rulings 203-207); decoration_unique is unchanged and stays statement-carried via [Fintype V]. ChoiceCannotBe entries updated. Root documents and the AFA Addendum script are held for editorial review and the PDF rebuild. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Qj4hZEe22hsY1FqfbKnnU2
…on uniqueness decoration_unique_of_val headlines (ruling 212); decoration_unique becomes the finite, graph-side Proposition (ruling 214). The false "infinite APGs ... not addressed" and "[Finite V] ... not measured" sentences are fixed; decoration_unique stays statement-carried via [Fintype V]. DA-1 Path 3 prose: K is now in the build via kolmogorov-complexity-lean and BrudnoBridge; Path 3's argument is not formalized (ruling 213). Dated searches name "the Mathlib then pinned (5450b53)". APG.lean Engineer's Take gains Tim's sentence (ruling 211). README, register, CLAIMS and LEAN_CUSTOM_REGISTRY updated. Editorial review PASS recorded. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Qj4hZEe22hsY1FqfbKnnU2
…tations, choice counts) Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Qj4hZEe22hsY1FqfbKnnU2
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
All review gates recorded PASS; pre-push pipeline green.