land(mirrormere): the six verified team branches, integrated serially (4 proofs + 4 emitter kinds) - #577
Merged
Conversation
…rade) Discharges the two T1-track registry nodes of the torus-section ladder (QC_TORUS_SECTION_LADDER_MEMO_2026-09-14, sections 5-6) in one new quasicrystal-island artifact, TorusSectionLadder.lean, sorry-free: torus_section_dictionary (MM_torus_section_dictionary, draft) torus_section_n2_rigidity (MM_torus_section_n2_rigidity, open) Both theorem lines are VERBATIM from the registry statement files; the three ladder definitions (torusOrbit, linearTorusForm, expSum) are mirrored verbatim from MMDefs.lean:69-76 into the module's own Quasicrystal namespace, following the E6Bridge.lean precedent, so the normalized-containment grant gate matches. GRADE, recorded rather than hidden: both are vocabulary bridges, NOT mathematics. The dictionary is a Fin-2 sum unfolding closed by one simp; the rigidity rung is a one-line rewrite into the island's already-proved twoFreq_realRooted_iff. Its registry kind "milestone" is inflated (it is a lemma). NEITHER IS COUNTED AS A WIN. The general-N identity is rfl and is kept only as an explicit vocabulary anchor, not as a node. No new Telperion emitter kind was built and none is missing: the shape is a variable map between two vocabularies, already classified by VarMapAdapterEmitter / ReparamAdapterEmitter (both STRUCTURALLY_NONVACUOUS, "no new identity"). Registry: mission link + attempt recorded on both nodes. NO grant -- the dictionary is still draft pending its post-revision re-audit, and the artifact lives on the climb branch while the registry lives on main, so the grant is deferred to the branch reconcile like every other climb-linked node. The containment gate was dry-run offline: statement found in artifact for both. Registered TorusSectionLadder as lean_lib + defaultTarget; added three #print axioms lines to AxiomGuardQC.lean. lake build: 3116 jobs successful. Guard: 45 theorems, all [propext, Classical.choice, Quot.sound], no sorryAx. selfinversive_rigidity drift gate: OK (byte-for-byte). No RH progress is claimed. conjecture1_proved = False. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…ersive offline cert mode
MIRRORMERE torus-section ladder rung T2, THE NEGATIVE CONTROL. The p = 2 Euler
factor 1 - 2^(-s), read on s = 1/2 + ix as twoFreq(1, -(1/sqrt 2); 0, -log 2), is
NOT real-rooted: its zeros sit uniformly at Im x = 1/2. Registry statement proved
VERBATIM and sorry-free (statement_match_check all_match=True).
Lean (quasicrystal island, Mathlib v4.32.0), EulerFactorOffline.lean, namespace
TorusSectionLadder:
* euler_factor_section_offline -- the node. .mp of twoFreq_realRooted_iff would
force ||1|| = ||-(1/sqrt 2)||, i.e. 1 = 1/sqrt 2, refuted via one_lt_sqrt_two.
* euler_factor_section_witness -- the EXPLICIT off-line zero x = i/2
(e^{(log 2)/2} = sqrt 2), so the negative control carries a witness.
* euler_factor_section_witness_im + euler_factor_section_offline_of_witness --
Im (i/2) = 1/2 and the same refutation re-derived from the witness alone.
Telperion: SelfInversiveRigidityEmitter gains mode="offline" -- the refutation-shaped
mirror of the equal-modulus mode. Radical coefficients r*sqrt(q) keep |c|^2 = r^2*q
exact; frequencies may be r*log q; verdict |c1|^2 != |c2|^2 emits NOT-real-rooted with
the kernel re-deriving both norms by norm_num; the Euler-factor shape also ships the
x = i/2 witness and a registry-VERBATIM restatement. Negative control of the mode:
EQUAL modulus is REFUSED, as is any frequency pair whose distinctness would need
transcendence of log. Dogfooded on p = 2, 3, 5 (SelfInversiveOfflineInstances.lean,
18 theorems; p = 3, 5 are not nodes); existing selfinversive_rigidity drift check
covers both libs; 6 new tests (13 pass).
Registered in the island lakefile defaultTargets, AxiomGuardQC (18 new #print axioms,
all [propext, Classical.choice, Quot.sound], no sorryAx) and the CI job; mission link
+ attempt recorded, grant deferred to branch reconcile. Report:
telperion/docs/MM_mm-euler-factor-offline_2026-09-18.md.
Module named EulerFactorOffline, not TorusSectionLadder: worktrees sharing one built
.lake share the olean dir, and a teammate's same-named module silently clobbered mine.
conjecture1_proved = False. A finite, unconditional NEGATIVE control; no RH progress.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…cement (MIRRORMERE T2)
New emitter kind `twofreq_offline` (TwoFreqOfflineEmitter): the NOT-real-rooted
direction of the quasicrystal island's `twoFreq_realRooted_iff`, certified from the
EXACT rational inequality |c1|^2 != |c2|^2. The exact COMPLEMENT of
`selfinversive_rigidity`: the two emitters partition the coefficient space, each
REFUSING precisely the regime the other certifies, so neither can emit a false theorem.
Adds the literal shapes the rigidity emitter cannot express -- inv_sqrt(s, sign),
real_sqrt(q, s) and the -(Real.log p) frequency -- which is what the MIRRORMERE node
MM_euler_factor_section_offline needs (its coefficient is the irrational -1/sqrt 2).
That turns the single node into the whole ladder T2 family: for every p >= 2 the Euler
factor 1 - p^(-s) read on s = 1/2 + i x is the section twoFreq 1 (-(1/sqrt p)) 0
(-(log p)), never real-rooted; in `displacement` mode the emitter also certifies WHERE
the zeros go -- uniformly at Im x = 1/2, i.e. on Re s = 0.
Anti-phantom refusals (exact rational arithmetic, no floats): equal modulus (the sum IS
real-rooted, so the emitted negation would be FALSE); a zero coefficient; equal
frequencies including the disguised neglog(1) = rat(0); a negative rational frequency
opposite a -log p frequency; a radicand that is not an integer >= 2; displacement mode
outside the Euler-factor shape; p < 2.
Verified locally on the v4.32 quasicrystal island:
* lake build EulerFactorSectionOffline -- green, 8 theorems, no warnings, no sorry
* #print axioms on all 8 -- [propext, Classical.choice, Quot.sound]
* telperion.statement_match -- 2/2 kernel-level defeq match, so the p=2 theorem
states EXACTLY the MM node proposition (not merely string containment)
* generic_negative_control -- kernel_rejects=True on the equal-modulus forgery
(fails with h2 : True |- False), true_compiles=True on the p=2 twin
* pytest: test_emit_twofreq_offline 13 passed, test_negctrl_twofreq_offline 7 passed,
test_certificate_sensitivity 12 passed/30 skipped, test_emitter_registry 197
passed/62 skipped
Wiring: certify._SPECIAL_KINDS/_SPECIAL_DISPATCH, telperion.__init__ exports,
emitter_sensitivity.REGISTRY (STRUCTURALLY_NONVACUOUS + NEG_CONTROL_ADAPTER),
negctrl_adapters/__init__, telperion.toml [[check]] (group quick), quasicrystal
lakefile [[lean_lib]] (NOT in defaultTargets until CI is green), CI job
`twofreq-offline-compiles` (workflow re-parsed strictly, no duplicate keys, 75 jobs),
docs/EMITTER_MIRRORMERE_2026-09-18.md + catalog addendum.
Mission registry (via the CLI only): MM_euler_factor_section_offline LINKED to the
island artifact, attempt recorded [Proved]; NOT granted -- deferred to the
main/million-turing reconcile. `mission verify mirrormere` OK.
Honest scope: a finite fact about single Euler factors. Nothing about zeta, the Euler
product, or RH; read positively it certifies that per-rung line membership FAILS, so
critical-line membership can only be an infinite-N continuation phenomenon.
conjecture1_proved = False.
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
…iscs emitter kind Closes the registry node MM_offline_disjoint_discs (QC_RECURRENCE section 4.3 isolation lemma) sorry-free on the quasicrystal island, and builds the certificate kind the node's downstream consumer (the E5 Rouche template) was missing. conjecture1_proved = False. Nothing here is progress on RH: the lemma is elementary metric topology over an arbitrary Finset of points, and the emitted instances take their points as INPUT, asserting nothing about zeta's zeros. THE LEMMA (examples/quasicrystal/lean/OfflineDiscs.lean, new lean_lib + defaultTarget). The node statement is mirrored VERBATIM into the island's Quasicrystal namespace (diff against Statements/MM_offline_disjoint_discs.lean is empty modulo the stripped ":= by sorry"; node sha256 bac57ccef7c3f828). The proof sidesteps Finset.inf' non-emptiness bookkeeping entirely via a Finset.induction helper exists_pos_lower_bound_of_finset, applied to the offDiag distance image and the strip-margin image; r := min (eps1/3) (eps2/2), disjointness by Metric.closedBall_disjoint_closedBall, containment by the 1-Lipschitz abs_re_sub_le_dist (Complex.abs_re_le_norm). Empty and singleton cases fall out with no case split. THE KIND (src/telperion/emit_disjoint_discs.py, kind "disjoint_discs"). No existing emitter fit: two_scale_separation is one centre with two radii and no containment clause. Certificate = Gaussian-rational strip points + an explicit rational radius; exact self-check of the strict pairwise (2r)^2 < dist^2 and the strict strip margins. Emitted Lean eliminates the square root with Real.lt_sqrt BEFORE any arithmetic, so every kernel goal is rational norm_num, and the assembly theorem restates the registry node's existential at the concrete Finset, guarded by a statement_match example. Stance CERTIFICATE_SENSITIVE with a real Layer-2 seam: an inflated radius makes a pair theorem genuinely FALSE, not merely unprovable. negctrl_adapters/ adapter_disjoint_discs.py forges r = 1/10 on points 1/10 apart and the control passes two-sided (kernel REJECTED the forged FALSE proof | TRUE twin compiled clean). Layer 1 additionally refuses boundary-reaching radii, off-strip points, duplicates, and r <= 0. Also: examples/disjoint_discs/generate.py (two instances, incl. an off-line pair bank) emitting OfflineDiscsInstances.lean into the island, listed in telperion.toml as a quick-group drift gate; AxiomGuardQC extended with all five new decls (all [propext, Classical.choice, Quot.sound], 0 sorryAx); CI job disjoint-discs-compiles; 8 unit tests; report docs/MM_mm-offline-disjoint-discs_2026-09-18.md; catalog addendum. Registry touched only through the mission CLI: proof link + a Stalled attempt. The node is NOT granted here -- the grant gate belongs on main after reconcile. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…s of Real.exp
New first-class emitter: rational enclosures of Real.exp at a rational point,
re-derived in the kernel from Mathlib's Real.exp_bound. Four faces: exp,
exp_neg, deficit (e^x + e^-x - 2) and cosh. The exact rational order-n Taylor
box [S - r, S + r] (S = sum_(m<n) x^m/m!, r = |x|^n (n+1)/(n! n)) is computed
exactly; the generator selects the LEAST order whose box fits the CLAIMED
bracket and REFUSES every claim the box does not imply -- it never widens a
claim, and also refuses |x| > 1, order < 1 or > 64, an inverted bracket, a
non-positive deficit displacement, and non-rational (incl. float) input.
WHY: MM_bragg_defect_witness carries its e^(1/10) enclosure as the Arb
hypothesis hexp, and its read-back keeps closure_clean = false "until that
enclosure is itself reflected". The registry had no exp face at all
(transcendental_enclosure ships log only; log_combination uses exp_bound' as an
internal step). Dogfood instance (i) exp_tenth_bracket carries BraggDefect's
own 40-digit expLo/expHi literals (read out of BraggDefect.lean at generate
time, so driver drift breaks --check here), order 14; the bridge lemma
bragg_defect_witness_unconditional := BraggDefect.bragg_defect_witness
exp_tenth_bracket_defs
states the node's witness with NO hypothesis. The hypothesis-carrying form is
kept for the registry's syntactic grant gate and is itself gated by an
`open BraggDefect in example` reproducing the node statement. Instances (ii)
and (iii) bracket the recurrence deficit at d = 1/10 (BraggDefect.excess_bracket
constants; QC_RECURRENCE row a) and d = 1/5 (defect_eq_two's second channel);
(iv) reproduces ZooDH's order-6 cosh bracket constants.
Local verification (v4.32 zzl_aux island, shared built cache):
lake build ExpEnclosureInstances -- GREEN (8663 jobs, no errors)
axioms of all 4 instances + all 3 bridge theorems:
[propext, Classical.choice, Quot.sound]
two-sided negative control against the real kernel: forged bracket
[1, 1105/1000] REJECTED, true twin [110517/100000, 110518/100000] ACCEPTED.
Wiring: certify._SPECIAL_KINDS/_SPECIAL_DISPATCH, __init__ exports,
emitter_sensitivity.REGISTRY (STRUCTURALLY_NONVACUOUS + NEG_CONTROL_ADAPTER),
negctrl_adapters/adapter_exp_enclosure.py, telperion.toml [[check]]
exp_enclosure (quick), CI job exp-enclosure-compiles (strict duplicate-key YAML
parse: 75 jobs, no duplicates), README + NEW_EMITTERS_SUMMARY catalog rows.
Tests: tests/test_emit_exp_enclosure.py (22 passed),
tests/test_negctrl_exp_enclosure.py (7 passed); test_certificate_sensitivity
12 passed / 30 skipped and test_emitter_registry 197 passed / 62 skipped stay
green. Mission ledger: one `mission attempt MM_bragg_defect_witness` (Stalled)
recorded via the CLI -- no grant, no node edits by hand.
Scope: a finite arithmetic fact about transcendental constants at four rational
points, plus one NUMERIC hypothesis discharge. It does not enlarge what the
BraggDefect experiment says and the experiment's other trust seams (BraggH100's
Arb sign boxes, hLine) are untouched. conjecture1_proved = False.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…dentity emitter
Discharges the Face 4 (Bagchi recurrence) <-> Face 1 (Bragg/Weil defect)
dictionary row of QC_RECURRENCE section 2 row (a) / section 4 item 2, on the
zeta_zero_localization island (v4.32.0, shard zzl_aux).
Artifact: examples/zeta_zero_localization/lean/RecurrenceDeficit.lean
theorem recurrence_deficit_eq_excess -- node statement VERBATIM
recurrenceDeficit (1 / 10) = excess and 0 < recurrenceDeficit d for 0 < d
theorem recurrence_deficit_sq_eq_abs_defect -- companion, NOT a node
recurrenceDeficit is mirrored BYTE-IDENTICALLY from the registry vocabulary
mirror MMDefs.lean (lines 61-62) into the same namespace Quasicrystal, as the
rvm_bridge E6Bridge modules do; excess is verbatim BraggDefect vocabulary.
Sorry-free; axioms [propext, Classical.choice, Quot.sound] via AxiomGuardBragg.
NEW certificate kind exp_laurent_identity (ExpLaurentIdentityEmitter): an
identity in e^d, e^(-d) certified as an EXACT reduction of lhs - rhs modulo the
single relation e^d * e^(-d) = 1 in Q[y, z]; the quotient (cofactor) is the
load-bearing certificate carried into linear_combination. Refuses a nonzero
remainder and a cofactor-0 plain ring identity. Two-sided kernel-gated negative
control registered and passing -- the forged FALSE twin is the memo's own
corrected mistake (the clearances' SUM substituted for their PRODUCT).
Generator examples/exp_laurent_deficit/generate.py emits ExpLaurentDeficit.lean
into the zzl island; registered in telperion.toml ([[check]], group quick).
Registry (mission CLI only): proof link recorded on the open node + Proved
attempt in the ledger; mission grant DEFERRED to the branch reconcile per
mission.toml design section 9. mission verify mirrormere: OK.
SCOPE: a one-relation ring identity plus a two-factor positivity -- a dictionary
row between two finite, synthetic instruments, not an analytic theorem and not
evidence about zeta. No RH progress. conjecture1_proved = False.
Report: telperion/docs/MM_mm-recurrence-deficit_2026-09-18.md
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
# Conflicts: # telperion/missions/mirrormere/attempts.jsonl
# Conflicts: # telperion/docs/SECOND_PASS_EMITTER_CATALOG.md # telperion/examples/quasicrystal/lean/AxiomGuardQC.lean # telperion/examples/quasicrystal/lean/lakefile.toml # telperion/missions/mirrormere/attempts.jsonl # telperion/src/telperion/negctrl_adapters/__init__.py
# Conflicts: # telperion/missions/mirrormere/attempts.jsonl # telperion/src/telperion/negctrl_adapters/__init__.py
# Conflicts: # telperion/examples/zeta_zero_localization/lean/zzl_aux/lakefile.toml # telperion/missions/mirrormere/attempts.jsonl # telperion/src/telperion/__init__.py # telperion/src/telperion/certify.py # telperion/src/telperion/emitter_sensitivity.py # telperion/src/telperion/negctrl_adapters/__init__.py
# Conflicts: # .github/workflows/telperion-lean-e2e.yml # telperion/examples/quasicrystal/lean/AxiomGuardQC.lean # telperion/examples/quasicrystal/lean/lakefile.toml # telperion/missions/mirrormere/attempts.jsonl
The exp-enclosure merge's repair was left unstaged, so the merge commit captured the broken file. Staged now; the committed __init__.py parses. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
# Conflicts: # .github/workflows/telperion-lean-e2e.yml # telperion/docs/SECOND_PASS_EMITTER_CATALOG.md # telperion/missions/mirrormere/attempts.jsonl # telperion/missions/mirrormere/nodes/MM_euler_factor_section_offline.toml # telperion/src/telperion/__init__.py # telperion/src/telperion/certify.py # telperion/src/telperion/emitter_sensitivity.py # telperion/src/telperion/negctrl_adapters/__init__.py # telperion/telperion.toml
…ed artifact
Two defects the integration introduced or inherited, both caught by elaborating the
artifacts rather than by reading the diff:
1. Union merging produced THREE defaultTargets keys in the island lakefile, which Lake
rejects outright ('cannot redefine value key'), so every module on the island failed
to elaborate and disjoint-discs-compiles went red. Merged into one list of 12 targets,
union of all three, order preserved.
2. EulerFactorSectionOffline.lean -- the artifact I chose as MM_euler_factor_section_offline's
proof link when the gate tied -- was declared as a lean_lib but NOT in defaultTargets and
NOT in the island axiom guard. That is the same shape as the hole the 2026-09-18 audit
found (a node proved against Lean nothing compiles). It is now a defaultTarget and its 8
theorems are guarded; all 8 print exactly [propext, Classical.choice, Quot.sound].
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…ts + glued lean_lib) Same class as the quasicrystal repair: union merging duplicated defaultTargets and glued two [[lean_lib]] names into one block, so Lake refused the file and exp-enclosure-compiles went red. Merged the target lists (20 targets), gave ExpEnclosureInstances its own header. Swept every lakefile in the tree: no duplicate libs, no target without a declaring lean_lib. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The job built only OfflineDiscs and OfflineDiscsInstances, then ran AxiomGuardQC.lean, which imports every module on the quasicrystal island. The partial build left those imports unbuilt and the guard died with 'unknown module prefix LeeYangCore' -- a false red on proofs that are fine. Build all default targets first, as gram-inertia-compiles already does. The island is small, so this costs little. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
DrMurphyIsIn
added a commit
that referenced
this pull request
Sep 19, 2026
grant(mirrormere): four nodes proved after the team-branch landing (#577)
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
2 participants
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.
Lands the work that was already proved and verified but never merged, from the 2026-09-18 Mirrormere team run. Integrated serially into one branch rather than as six PRs, because all six touch the same four registry files and the C1 hazard in the team report is exactly that they clobber each other.
Proofs (each sorry-free and axiom-clean, independently verified during the run): the torus-section T1 rung, the E4b disjoint-discs isolation lemma, the recurrence-deficit identity, and the Euler-factor section off-line negative control.
Emitter kinds:
twofreq_offline,exp_enclosure,disjoint_discs,exp_laurent_deficit, each with its generator registered in the manifest and its drift gate green here.C4 resolved. Two branches proof-linked
MM_euler_factor_section_offlineto different modules. I ran the gate against both: both match, so the gate could not decide it. Chose the emitter-generatedEulerFactorSectionOffline.leanbecause it is regenerable and drift-gated, so a later edit that breaks it fails CI; the hand-writtenEulerFactorOffline.leanstays as an unlinked companion. Rule for the next tie: when the gate is indifferent, take the stronger guarantee against future drift.Integration notes, because union merging is not safe here. Union-merging the shared registry files silently produced three corruptions that no conflict marker announces: an eaten closing parenthesis where both sides ended an import block, a dropped manifest section header that made one entry absorb the next, and two spliced dictionary entries. Each was caught by parsing rather than by reading. The workflow file was never union-merged; it is rebuilt as main's file plus genuinely-new jobs, which also prevents resurrecting the retired monolith job that these branches predate. One commit here fixes a repair I had left unstaged.
Verification: registry, emitter and certificate suites 600 passed; all four campaigns verify OK; all four new drift gates green; manifest at 134 checks with no duplicates; workflow strict-parsed with no job missing relative to main.
Grants for the four proved nodes follow once this is on main and their island jobs are green. No node status changes in this PR.
conjecture1_proved = False.🤖 Generated with Claude Code