Horadam companion-matrix theory

[qazW12345]

Held fork-side validation PR for the Horadam companion-matrix submission.

Trusted base: 9f708c18fccb311646b10af124c60ca70e41857b
Final frozen candidate: bfa1591baa2872f43c224a39b9e9f6ceaabc6c94

This candidate contains the generic Horadam/Mathlib companion-matrix bridge plus a restrained Fibonacci/Lucas specialization module. It remains a fork-local development/validation checkpoint and must not be merged as part of validation.

Exact-head evidence

Fork CI on exact candidate bfa1591baa2872f43c224a39b9e9f6ceaabc6c94:

• test: SUCCESS — run 34962254980
• canonical validate-submission: SUCCESS — run 34962254942, job 104358343827
  • trusted base checkout: 9f708c18fccb311646b10af124c60ca70e41857b
  • candidate checkout: bfa1591baa2872f43c224a39b9e9f6ceaabc6c94
  • receiver accepted: true
  • diagnostics: none
  • build: pass
  • kernel recheck: pass
  • downstream import smoke: pass
  • Mathlib exact matches: 0
  • receiver observed exactly three changed files: the generic module, specialization module, and one claim JSON

OCI diagnostic 9:

• ops control head: 09f92bd62132bc2f1a344c5764d976f2b40b7ce6
• run 34962274290, job 104358407986
• exact pin: trusted 9f708c18fccb311646b10af124c60ca70e41857b, candidate bfa1591baa2872f43c224a39b9e9f6ceaabc6c94
• trusted preflight: pass
• diagnostic lake build: pass (2299 jobs)
• kernel recheck: pass
• Mathlib exact matches: 0
• restricted receiver failed only at the known self-hosted ARM downstream-import smoke timeout: lake env lean /tmp/leanfrontier/downstream/Client.lean exceeded the fixed 30-second limit. The canonical GitHub-hosted receiver passed the same downstream import on this exact candidate.

Repair history

Historical candidate 9b6d6602832d89036fb2b48b8ddd6e80e92a8c36 (including OCI ops head 4cce5b0779185917597162a6590a68aba74954eb) had a clean diagnostic Lake build and kernel recheck but was rejected because the expanded positive-power characteristic-polynomial theorem exceeded the normalized-term limit. That was repaired through ordinary public mathematical API companionPowerCharPoly, not by changing trusted limits.

Historical candidate addd754b4b0da9162cbf5bee161b18697243b90c then passed test but canonical validate-submission run 34942857171, job 104295326076, failed with the receiver's generic BUILD_FAILED: error: build failed. OCI diagnostic 7 pinned that exact candidate at ops head 23be57dad51d3a7f62e9f56b03112bf2e3ec23d3; run 34942878054, job 104295387947, gave the actionable compiler error at HoradamCompanionMatrix.lean:146:4: companionPowerCharPoly failed to compile and should be marked noncomputable because it depends on noncomputable polynomial addition. Commit fbbb8b8a1bd6faea5d2ef71615c5e34cfe98455c applied exactly that ordinary-source one-line repair. Its exact-head test run 34943560907 and canonical validate-submission run 34943560879 both passed. No trusted receiver rule or limit was changed.

Review boundary

Owner adversarial review has pressure-tested recurrence signs, index shifts, Q = 0, Fibonacci P = 1, Q = -1, natural-to-integer coercions, Lucas base cases, and charpoly assumptions. No unresolved owner defect remains. Independent review is still required before any upstream submission/merge; owner review and CI do not substitute for it.

Do not merge this fork-local PR as part of validation.

[qazW12345]

Validation checkpoint for exact candidate df57840413d642b3ad89c3b6dceb29b881c2c068 against trusted base 9f708c18fccb311646b10af124c60ca70e41857b:

• OCI diagnostic run 34939468533: trusted preflight PASS; full diagnostic lake build PASS (2298 jobs); kernel recheck PASS. Restricted validation reports exactly one failure: the known 30-second downstream-import smoke-test timeout on the 2-core ARM OCI host.
• Canonical fork validate-submission run 34940409332 on the same exact base/head: PASS, including Restricted formal validation, downstream import smoke test, kernel recheck, 118 corpus entrypoints checked, and zero diagnostics.
• Canonical receiver report artifact: 10384948265, digest sha256:8ed77659a22028e7fd08f856ac4c63570378edfc7c8e825d17f95f026719e1c8.

Conclusion: no further candidate repair is indicated by validation evidence. The OCI failure is host-specific timeout evidence, not a compiler/elaborator or trusted-policy failure. Keep this PR held/draft; do not merge it as part of validation.

[qazW12345]

Frozen-candidate owner review checkpoint for exact head bfa1591baa2872f43c224a39b9e9f6ceaabc6c94 against trusted/upstream main @ 9f708c18fccb311646b10af124c60ca70e41857b.

Fresh live verification:

• test run 34962254980: SUCCESS on exact head bfa1591....
• canonical validate-submission run 34962254942, job 104358343827: SUCCESS on exact base/head; receiver accepted: true, diagnostics none, build pass, kernel recheck pass, downstream-import smoke pass, 118 corpus entrypoints checked, Mathlib exact matches 0.
• receiver artifact 10393948731, digest sha256:3b1f9d64e5d188e0db94f7f1019bf4a5c4be9c0dcec7a1e882df163475133c8b.
• upstream main is still exactly 9f708c18fccb311646b10af124c60ca70e41857b, so no rebase/revalidation is currently required.

Adversarial owner review found no source/provenance defect. The generic matrix/recurrence signs and index shifts remain correct for n=0, n=1, Q=0, and P=0; Nontrivial is confined to the charpoly bridge where needed. For the Fibonacci specialization, P=1,Q=-1 gives exactly the accepted Fibonacci Q-matrix, the two-step Horadam/Fibonacci bridge has correct bases and recurrence, and the positive-power trace specializes to F n + F (n+2) = L(n+1). The existing FibonacciMatrix module already exposes the Fibonacci-sum trace and LucasNumber exposes the Fibonacci/Lucas bridge separately, so trace_fibMatrix_pow_succ_eq_lucas is a genuine API composition bridge rather than an exact alias/restatement; the trusted receiver independently reports alias: false, restatement: false and zero Mathlib exact matches.

The claim boundary is also consistent with the contract: the three specialization theorems are now explicit entrypoints; supporting mathematical definitions remain public API without being claim entrypoints; statement_origin=machine and proof_origin=machine correctly describe formal authorship while human topic selection is recorded in source_context.

No independent review is present yet, so this remains owner evidence only. Keep this PR draft/held and do not merge it. Upstream PRs carlok#179 and carlok#180 remain open, and the cadence question on carlok#180 is still unanswered; do not open another upstream PR until that boundary changes or an explicit decision overrides it.

[qazW12345]

NEW SESSION HANDOFF — Horadam companion-matrix submission

This comment is intended to be a self-contained resume checkpoint for a fresh agent/session. Resolve live GitHub state before acting, but if the coordinates below are unchanged, do not reopen already-resolved repairs.

Authoritative coordinates

• Fork: qazW12345/LeanFrontier
• Upstream/trusted receiver: carlok/LeanFrontier
• Fork PR: Horadam companion-matrix theory #4 — Horadam companion-matrix theory
• Development branch: submission/horadam-companion-matrix
• Trusted/upstream base: 9f708c18fccb311646b10af124c60ca70e41857b
• Frozen candidate: bfa1591baa2872f43c224a39b9e9f6ceaabc6c94
• PR Horadam companion-matrix theory #4 is intentionally open + draft + held, and must not be merged as part of validation.

Current candidate changes exactly three files:

1. LeanFrontier/LinearAlgebra/HoradamCompanionMatrix.lean
2. LeanFrontier/LinearAlgebra/HoradamCompanionMatrixSpecializations.lean
3. Submissions/horadam-companion-matrix.json

Mathematical scope

The generic module bridges the existing LeanFrontier.Horadam.W recurrence to Mathlib LinearRecurrence, defines the 2×2 companion matrix [[P,-Q],[1,0]], proves state propagation and powers, determinant/trace formulas, and characteristic-polynomial results. Supporting API includes recurrence, companionMatrix, companionPowerFormula, and noncomputable companionPowerCharPoly.

The specialization module deliberately stays separate and connects the generic theory to the repository's existing Fibonacci/Lucas API:

• LeanFrontier.Horadam.companionMatrix_fibonacci
• LeanFrontier.Horadam.W_fibonacci_eq_fib
• LeanFrontier.Horadam.trace_fibMatrix_pow_succ_eq_lucas

The claim JSON currently names 14 theorem entrypoints:

• LeanFrontier.Horadam.W_isSolution_recurrence
• LeanFrontier.Horadam.recurrence_charPoly
• LeanFrontier.Horadam.companionMatrix_mulVec_W_state
• LeanFrontier.Horadam.companionMatrix_pow_mulVec_initial
• LeanFrontier.Horadam.companionMatrix_pow_succ
• LeanFrontier.Horadam.det_companionMatrix
• LeanFrontier.Horadam.det_companionMatrix_pow
• LeanFrontier.Horadam.trace_companionMatrix
• LeanFrontier.Horadam.trace_companionMatrix_pow_succ_fundamental
• LeanFrontier.Horadam.charpoly_companionMatrix
• LeanFrontier.Horadam.charpoly_companionMatrix_pow_succ_fundamental
• LeanFrontier.Horadam.companionMatrix_fibonacci
• LeanFrontier.Horadam.W_fibonacci_eq_fib
• LeanFrontier.Horadam.trace_fibMatrix_pow_succ_eq_lucas

Exact-head validation evidence

For exact candidate bfa1591baa2872f43c224a39b9e9f6ceaabc6c94 against trusted base 9f708c18fccb311646b10af124c60ca70e41857b:

• test run 34962254980: SUCCESS
• canonical validate-submission run 34962254942, job 104358343827: SUCCESS
  • exact trusted checkout: 9f708c18...
  • exact candidate checkout: bfa1591...
  • receiver accepted: true
  • diagnostics: none
  • build: pass
  • kernel recheck: pass
  • downstream import smoke: pass
  • 118 corpus entrypoints checked
  • Mathlib exact matches: 0
• canonical receiver artifact: 10393948731
• artifact SHA-256: 3b1f9d64e5d188e0db94f7f1019bf4a5c4be9c0dcec7a1e882df163475133c8b

OCI diagnostic harness

Live OCI control branch/checkpoint at handoff:

• ops/oci-validator @ 09f92bd62132bc2f1a344c5764d976f2b40b7ce6
• .github/oci-validation-target pins trusted 9f708c18... to candidate bfa1591...
• request horadam-companion-matrix-diagnostic-9-2026-09-15
• run 34962274290, job 104358407986

Diagnostic result:

• trusted preflight: pass
• Diagnostic Lake build: PASS — 2299 jobs
• both Horadam modules compile
• restricted receiver reports build pass + kernel recheck pass + zero Mathlib exact matches
• only failure: downstream consumer import lake env lean /tmp/leanfrontier/downstream/Client.lean exceeds the fixed 30 second smoke timeout on the self-hosted 2-core ARM OCI machine

This is a known host-specific OCI condition. Do not repair Lean source or weaken trusted receiver timeout/rules in response to this timeout when the same exact candidate passes the canonical hosted receiver. Diagnostic Lake build is the primary compiler/elaborator signal.

Important repair history — do not regress to old watcher SHAs

Watcher events may replay older checkpoints. Always compare the reported SHA with the live control file/PR head before acting.

• Historical candidate 9b6d6602832d89036fb2b48b8ddd6e80e92a8c36: Lake build + kernel recheck passed, but the expanded positive-power charpoly theorem exceeded the trusted normalized-term resource limit. Fixed by introducing ordinary mathematical API companionPowerCharPoly; trusted limits were not changed.
• Historical candidate addd754b4b0da9162cbf5bee161b18697243b90c: canonical receiver gave generic build failure. OCI diagnostic 7 (ops @ 23be57dad51d3a7f62e9f56b03112bf2e3ec23d3) exposed the exact Lean error: companionPowerCharPoly had to be noncomputable because polynomial addition is noncomputable. Commit fbbb8b8a1bd6faea5d2ef71615c5e34cfe98455c applied exactly that one-line ordinary-source repair; exact-head test + canonical receiver then passed.
• ec62e865421d977079023a1f1ec88bddb47be58f added the Fibonacci/Lucas specialization module; child bfa1591... updated the claim metadata so the three specialization theorems are explicit entrypoints. bfa1591... is the frozen final candidate.

Owner adversarial review already completed

Owner/self-review has tried to falsify the important boundaries rather than merely rereading the proofs:

• recurrence sign convention W(n+2) = P*W(n+1) - Q*W(n) vs coefficients [-Q,P]
• state-vector orientation and matrix [[P,-Q],[1,0]]
• n=0 and n=1 power/trace cases
• degenerate P=0 and singular Q=0 cases; no accidental invertibility/field assumption
• determinant sign (det = Q)
• Nontrivial confined to charpoly bridge where required
• Fibonacci specialization P=1,Q=-1 gives exactly [[1,1],[1,0]]
• Horadam/Fibonacci bridge checks both base cases and the recurrence/cast boundary
• Lucas trace index/sign: at n=0, trace fibMatrix = 1 = Lucas 1; at n=1, trace fibMatrix² = 3 = Lucas 2
• receiver classifies specialization theorems as alias: false, restatement: false
• provenance boundary: formal statement/proof text is machine-authored; human selected an agent-proposed direction but did not author/materially edit the Lean statements/proofs, so statement_origin=machine, proof_origin=machine is intentional
• no claim of new mathematics; contribution is formalization/integration of classical recurrence/matrix theory

No unresolved owner defect is known.

Remaining workflow gate

At this handoff there are zero submitted independent reviews on fork PR #4. Owner/self-review and CI do not count as independent review.

Therefore:

1. Keep bfa1591baa2872f43c224a39b9e9f6ceaabc6c94 frozen unless a genuinely new defect is found.
2. Do not self-approve PR Horadam companion-matrix theory #4 and do not treat owner review as independent acceptance.
3. Do not merge PR Horadam companion-matrix theory #4; it is a fork-local validation checkpoint.
4. Obtain a separate independent adversarial review of the exact frozen SHA before upstream submission/merge.
5. Upstream PRs feat(NumberTheory): add ordered Markov-tree descent carlok/LeanFrontier#179 and feat(Geometry): bridge Ford circles to Euclidean sphere tangency carlok/LeanFrontier#180 were still open at the last live check, and the cadence question on feat(Geometry): bridge Ford circles to Euclidean sphere tangency carlok/LeanFrontier#180 had no maintainer response. Do not open a third upstream PR unless that boundary changes or an explicit decision overrides it.
6. If upstream main, PR Horadam companion-matrix theory #4 head, claim, or source changes, re-resolve exact SHAs and require fresh exact-head validation/review as appropriate.

Fresh-session resume procedure

A new agent should start by reading this comment and PR #4 body, then verify live state instead of trusting the checkpoint blindly:

1. Fetch PR Horadam companion-matrix theory #4 and confirm base/head/draft/merge state.
2. Fetch ops/oci-validator:.github/oci-validation-target and resolve exact TRUSTED_REF/CANDIDATE_REF.
3. Check exact-head test and canonical validate-submission for the current candidate.
4. Check submitted reviews/review threads and upstream feat(NumberTheory): add ordered Markov-tree descent carlok/LeanFrontier#179/feat(Geometry): bridge Ford circles to Euclidean sphere tangency carlok/LeanFrontier#180/cadence status.
5. If live head remains bfa1591..., trusted base remains 9f708c18..., canonical validation remains green, and no independent review exists, do not modify source; the next task is independent review / cadence handling.
6. Only reopen the candidate repair loop for a defect on the current exact candidate, not for replayed watcher failures on superseded SHAs.
7. Never weaken trusted validation infrastructure, limits, or timeout policy to make a candidate pass.

This checkpoint is repository metadata only and intentionally does not modify the frozen candidate tree or invalidate its exact-head CI.