v0.2.42 dense routed exponent bound

Adds a formal upper-bound audit for the strongest currently available dense target-routed candidate.

Lean now proves:

• exact finite normalized saving 2368333/474989023199232 ≈ 4.986079434×10^-9 under the explicit free target-indexed routing premise;
• the corresponding finite epsilon is < 5×10^-9;
• for the inherited recurrence multiplier 13824·(1−epsilon), the exponent gap -log(1−epsilon)/log(13824) is strictly < 10^-9.

This is a route-specific conditional upper bound, not a lower bound for arbitrary complex circuits. It shows that eliminating the serialized switch charge alone cannot reach a 10^-9 exponent improvement. The actual phase transport q_U, charged complex factorization, scalar-gate schedule, and all-length recurrence remain open.

Validation: direct Lean compilation of DenseTargetRoutedFrameAudit.lean succeeded after the exact log/exponential inequalities were added.

v0.2.41 dense target routing and Walsh bridge

Formalized two local bridges for the dense two-frame candidate.

Included Lean certificates:

• target-indexed route (identity on the unit block, denseSwap on the dense block) maps the anchored unit label to the unique target-boundary label and has a monomial address lift;
• under an explicit free target-indexed routing premise, the switch charge is zero, with exact H24 finite normalized saving 2368333/474989023199232 ≈ 4.986079434×10^-9; this changes the inherited exponent gap only from about 5.229696371×10^-10 to 5.229698963×10^-10, still below 10^-9;
• a separated diagonal profile proves denseSwap does not leave every phase profile invariant; actual q_U transport remains open;
• the lifted dense swap is orthogonal and commutes with every scalar-normalized concrete binary Walsh matrix, so Walsh-framed phase conjugation is exact up to address relabelling.

Validation: lake build OAI.Computability.FourierCircuit.DenseTwoFrameWalshBridge (8976 jobs, success); direct Lean validation of DenseTargetRoutedFrameAudit succeeded. These are local/conditional semantic certificates and do not construct a charged complex shear, a global all-length schedule, or an unconditional exponent theorem.

v0.2.40 dense address-matrix bridge

Formalized the dense two-frame swap at the complex address-matrix level.

Included Lean theorems:

• exact conjugation of matrix units by the lifted binary address permutation;
• exact relabeling of arbitrary complex diagonal phase profiles.

Scope: these are free address/monomial semantics. They do not by themselves establish a charged complex shear, a global all-length DFT schedule, or an unconditional exponent theorem.

Validation: lake env lean -DautoImplicit=false OAI/Computability/FourierCircuit/DenseTwoFrameComplexBridge.lean (warnings only).

v0.2.39 dense frame switch witness

This release adds DenseBlockFrameSwitch.lean, a Lean-checked attachment of the dense two-frame route to an explicit finite block-order ledger.

At h=24 it proves:

• every weight-three target has exactly one eligible frame among u=e_0 and w=1+e_0;
• the serialized order [unit,dense] has exactly one switch;
• the weighted switch charge is 1202;
• the linked conditional margin is 2,425,171,790, with normalized value 1212585895/243194379878006784 > 10^-9.

The file explicitly treats the block order, physical gate realization, and global schedule as premises. It is a frame-routing certificate, not an unconditional exact-DFT circuit or exponent theorem.

Validation:

cd lean
lake env lean -DautoImplicit=false OAI/Computability/FourierCircuit/DenseBlockFrameSwitch.lean

v0.2.38 two-frame routing arithmetic

This release adds TwoFrameRoutingArithmetic.lean, a Lean-checked H24 arithmetic certificate for the dense two-frame target-routing candidate.

For the conditional accounting model, it proves:

• switch-only charge 1202, margin 2,425,171,790, normalized margin 1212585895/118747255799808 > 10^-6;
• block-roundtrip charge 55,292, margin 2,425,117,700, normalized margin 606279425/59373627899904 > 10^-6.

The label-level cover remains the pair u=e_0, w=1+e_0 at even width. These are route-candidate width margins, not an unconditional exponent theorem. A complex gate, direct source formation, global frame schedule, and all-length DFT recurrence remain open.

Validation:

cd lean
lake build OAI.Computability.FourierCircuit.TwoFrameRoutingArithmetic

v0.2.37 gate-level frame no-go

This release adds a Lean-checked gate-level attachment of the binary-to-complex frame obstruction.

BinaryComplexFrameMap.lean now proves no_unitShearWitness_fin2_support_transport: an actual ComplexShearGateBridge.UnitShearWitness, whose circuit is a concrete LinearDAG with one scalar Gate.add, cannot globally transport the support encoding of the smallest Fin 2 binary transvection. The proof reduces the circuit evaluation to its complex shear matrix and invokes the support no-go.

This is a route-specific semantic obstruction. It does not provide a lower bound for arbitrary complex circuits and leaves open multi-gate matrices, non-support frame invariants, and a global all-length schedule.

Validation:

cd lean
lake build OAI.Computability.FourierCircuit.BinaryComplexFrameMap

v0.2.36 explicit event schedule and pair direct-channel audit

Explicit event schedule and pair direct-channel audit

This release extends the h=24 conditional exponent-gap certificate.

New formal material

• CenterBoundaryExactEventSchedule.lean supplies the identity schedule on
  ThreeStageReturnEvent I h, proves the exact six-phase event count, and
  instantiates the existing strict 10^-9 exponent-gap inequality.
• pair_direct_channel_reaudit.py and its accompanying note compute the exact
  h=24 break-even direct-channel charge for the pair/complement side-wire
  candidate: 74/759 < 1. Any integral one-way direct charge is already
  negative under the current boundary ledger.

Scope

The event schedule is an abstract finite event witness. It is not a legal
complex gate schedule, a global frame-labelled DAG, or an all-length exact DFT
recurrence. The pair/complement result is a route-specific algebraic and cost
obstruction; it is not a lower bound for arbitrary complex circuits.

The previously proved conditional theorem remains:

1e-9 < -log(1 - epsilon) / log(13824)

under the six-phase ledger and inherited recurrence multiplier assumptions.

Validation

cd lean
lake build OAI.Computability.FourierCircuit.CenterBoundaryExactEventSchedule
python3 scripts/pair_direct_channel_reaudit.py

Public records

• Fork PR: #1
• Version release: https://github.com/whyihaveyou/math/releases/tag/v0.2.36-event-schedule-audit
• Previous version DOI: https://doi.org/10.5281/zenodo.23242745

v0.2.35 conditional exponent-gap audit

This release formalizes the analytic conversion from the six-phase conditional ledger to the recurrence exponent gap.

• FusedCentreExponentGapAudit.lean defines the inherited multiplier as m * (1 - epsilon) and the gap as -log(1-epsilon)/log(m).
• It proves log(13824) < 11 from a finite exponential-series bound and uses log(1-epsilon) <= -epsilon to establish the strict conditional inequality 1/10^9 < -log(1-epsilon)/log(13824).

The theorem is conditional on the six-phase event ledger and the inherited recurrence formula. It does not prove the missing selective complex gate, the global all-prefix schedule, or an all-length exact DFT theorem. The preceding v0.2.34 release is archived on Zenodo at DOI 10.5281/zenodo.23242451.

v0.2.34 naturality and dense-block audit

This release adds the next formal layer for the h=24 optimization audit.

• FusedCentreTransportNaturality.lean proves row-by-row naturality of the fused six-row invocation under four explicit intertwining laws for R, G, J, and V. It also proves pointwise address-transport round trips with arbitrary initial side and centre banks, and binds the tensor-lift transport to the sheared L5 boundary certificate.
• DenseBlockBoundaryArithmetic.lean and scripts/dense_block_boundary_audit.py record the exact h=24 dense two-frame block ranks. Both 253-target and 1771-target blocks have constraint rank 23; the target-indexed parity ranks are (252,253,23) and (1770,1771,23). Under the explicit one-switch-per-prefix premise, the conditional normalized margin is 1212585895/243194379878006784 (about 4.9861e-9).

These are local naturality, binary-span, and conditional-ledger certificates. They do not prove a selective complex gate, a global schedule, an all-length DFT recurrence, or a lower bound for arbitrary complex circuits. The preceding v0.2.33 release is archived on Zenodo at DOI 10.5281/zenodo.23241991.

v0.2.33 fusion-boundary audit

This release adds two Lean-checked route audits for the h=24 exact-DFT optimization program.

• CenterBoundaryFusionNoGo.lean proves that the scalar centre-fusion identity cannot enter the old row-5 boundary by adding a source-row vector already in L2. A future 10^-9 construction must supply a shear, change the boundary, or cancel the direct target term before row 5.
• DenseTwoFrameComplexBridge.lean formalizes the even-width dense two-label address-permutation bridge and proves that the binary support transport is not a single complex shear under the support-map semantics.

These are local frame and semantic certificates. They do not claim a physical global gate schedule, an all-length DFT recurrence, or an unconditional exponent improvement. The preceding v0.2.32 release is archived on Zenodo at DOI 10.5281/zenodo.23240807.