Energy.lean`

48 declarations, 0 contain sorry, 0 declared as axioms

Energy

Shaped envelopes, actual coefficient aggregation, role counts, central contributions, and full coefficient energy.

def OAI.TraceReconstruction.OccupiedParityTree.Forced.envelope line 26

Source documentation

Actual unsigned coefficient envelope on one ordered occupied shape. No bits are resampled for the additional leaves.

def Forced.envelope (T n g : ℕ → ℕ) (s : ℕ) (center : ℕ → ℤ)
    (globalShift : (b : ℕ) → (Fin (g b) → Bool) → Fin (T b) → ℤ)
    {b : ℕ} {t : OccupiedParityTree b} (F : t.Forced) (x : t.Labels T)
    (bits : WindowAssignments T n g Bool b) (incoming : ℤ) : ℝ :=
…

Mentions: OAI.TraceReconstruction.OccupiedParityTree, OAI.TraceReconstruction.WindowAssignments

def OAI.TraceReconstruction.OccupiedParityTree.Forced.averagedEnvelope line 34
def OAI.TraceReconstruction.OccupiedParityTree.Forced.extraOffsets line 43
Source documentation
Offsets for all extra leaf constraints, with only their labels replaced by zero. The location of each constraint is not changed by that replacement.
```
def Forced.extraOffsets (T n g : ℕ → ℕ) (hT : 0<T 0) (center : ℕ → ℤ)
    (globalShift : (b : ℕ) → (Fin (g b) → Bool) → Fin (T b) → ℤ)
    {b : ℕ} {t : OccupiedParityTree b} (F : t.Forced)
    (p : BinaryWindowLabels T b) (z : F.InteriorLabels T)
    (bits : WindowAssignments T n g Bool b) (incoming : ℤ) (e : F.ExtraLeafEdge) : ℤ :=
…
```
Mentions: OAI.TraceReconstruction.OccupiedParityTree, OAI.TraceReconstruction.BinaryWindowLabels, OAI.TraceReconstruction.WindowAssignments
theorem OAI.TraceReconstruction.OccupiedParityTree.Forced.averagedEnvelope_split line 51

theorem OAI.TraceReconstruction.OccupiedParityTree.Forced.envelope_energy line 82

Source documentation

Summing every actual numeric labeling of a fixed shape costs exactly one l1-squared factor per extra leaf and one factor per extra interior label. The forced-anchor energy remains a single genuine correlated posterior.

theorem Forced.envelope_energy (T n g : ℕ → ℕ) (hT : 0<T 0) (s : ℕ) (center : ℕ → ℤ)
    (globalShift : (b : ℕ) → (Fin (g b) → Bool) → Fin (T b) → ℤ)
    {b : ℕ} {t : OccupiedParityTree b} (F : t.Forced)
    (R : BinaryWindowLabels T b → Prop) [DecidablePred R]
    (d : WindowAssignments T n g (Option Bool) b) (incoming : ℤ) :
    (∑x : t.Labels T, if R (F.labels T x) then
      (F.averagedEnvelope T n g s center globalShift x d incoming)^2 else 0) ≤
      (Fintype.card (F.InteriorLabels T):ℝ) * ((2^s:ℕ):ℝ)^(2*Fintype.card F.ExtraLeafEdge) *
        ∑p : BinaryWindowLabels T b, if R p then
          (binaryAnchorAverage T n g s center globalShift b p d incoming)^2 else 0 := by
…

Mentions: OAI.TraceReconstruction.OccupiedParityTree, OAI.TraceReconstruction.BinaryWindowLabels, OAI.TraceReconstruction.WindowAssignments, OAI.TraceReconstruction.binaryAnchorAverage

theorem OAI.TraceReconstruction.OccupiedParityTree.Forced.envelope_energy_root line 125

Source documentation

Connected forced-shape coefficient-envelope estimate with the true common-global/local sibling energy, and no independent-sibling substitute.

theorem Forced.envelope_energy_root (T n g : ℕ → ℕ) (hT : 0<T 0) (s : ℕ)
    (center : ℕ → ℤ)
    (globalShift : (b : ℕ) → (Fin (g b) → Bool) → Fin (T b) → ℤ)
    (A : (b : ℕ) → Finset (Fin (T b))) (shift : ℕ → ℤ)
    (hplat : HasGlobalPlateau T g A shift globalShift)
    (B C : ℕ → ℝ) (hB : ∀b,0≤B b) (hC : ∀b,0≤C b)
    (b : ℕ) (t : OccupiedParityTree (b+1)) (F : t.Forced)
    (d : WindowAssignments T n g (Option Bool) (b+1))
    (hcap : MetadataBinomialCaps T n g B C (b+1) d) (incoming : ℤ) :
    (∑x : t.Labels T, if BinaryWindowLabels.allowed T A s (b+1) (F.labels T x) then
      (F.averagedEnvelope T n g s center globalShift x d incoming)^2 else 0) ≤
      ((Fintype.card (F.InteriorLabels T):ℝ) * ((2^s:ℕ):ℝ)^(2*Fintype.card F.ExtraLeafEdge)) *
…

Mentions: OAI.TraceReconstruction.HasGlobalPlateau, OAI.TraceReconstruction.OccupiedParityTree, OAI.TraceReconstruction.WindowAssignments, OAI.TraceReconstruction.MetadataBinomialCaps, OAI.TraceReconstruction.BinaryWindowLabels.allowed

def OAI.TraceReconstruction.OccupiedParityTree.Edge.bottomAddress line 156

Source documentation

The actual full-tree leaf address of a bottom edge, including the edge's own numeric label.

def Edge.bottomAddress (T : ℕ → ℕ) : {b : ℕ} → {t : OccupiedParityTree b} →
    (x : t.Labels T) → (e : t.Edge) → e.height=0 → WindowLeaf T b
  | _, .leaf, _, e, _ => e.elim
  | b+1, .node k children roles, x, Sum.inl i, he => by
      change b=0 at he
      subst b
      exact (x (Sum.inl i),(⟨0,by decide⟩ : Fin 1))
  | b+1, .node k children roles, x, Sum.inr z, he =>
      (x (Sum.inl z.1), Edge.bottomAddress T (x.child T z.1) z.2 he)

Mentions: OAI.TraceReconstruction.OccupiedParityTree, OAI.TraceReconstruction.WindowLeaf

theorem OAI.TraceReconstruction.OccupiedParityTree.Edge.bottomAddress_mem line 166

theorem OAI.TraceReconstruction.OccupiedParityTree.Edge.bottomIndicator_eq line 191

Source documentation

Leaf constraints read from the real shape label address are exactly the ones in the genuine complete-tree latent law.

theorem Edge.bottomIndicator_eq (T n g : ℕ → ℕ) (s : ℕ) (center : ℕ → ℤ)
    (globalShift : (b : ℕ) → (Fin (g b) → Bool) → Fin (T b) → ℤ)
    (b : ℕ) (t : OccupiedParityTree (b+1)) (x : t.Labels T)
    (e : t.Edge) (he : e.height=0)
    (bits : WindowAssignments T n g Bool (b+1)) (incoming : ℤ) :
    sourceBottomIndicator T n g s center globalShift b bits incoming (e.bottomAddress T x he) =
      motifIndicator s ((x e).val-sourceTreeAnchors T n g center globalShift (b+1) bits incoming
        (e.parentPath T x)) := by
…

Mentions: OAI.TraceReconstruction.OccupiedParityTree, OAI.TraceReconstruction.WindowAssignments, OAI.TraceReconstruction.sourceBottomIndicator, OAI.TraceReconstruction.motifIndicator, OAI.TraceReconstruction.sourceTreeAnchors

theorem OAI.TraceReconstruction.product_zero_one_pull_le line 238
Source documentation
Taking repeated constraints from a zero-one product can only enlarge it. The map need not be injective. This keeps the real leaf addresses, including coincident labels in the ambient enlarged summation.
```
theorem product_zero_one_pull_le {α β : Type*} [Fintype β]
    (S : Finset α) (f : α → ℝ) (hf : ∀a∈S,f a=0 ∨ f a=1)
    (g : β → α) (hg : ∀b,g b∈S) : (∏a∈S,f a)≤∏b,f (g b) := by
…
```

theorem OAI.TraceReconstruction.sourceRoleTerm_envelope line 255

Source documentation

Every actual role coefficient is bounded by its actual forced shape and extra-leaf envelope before averaging over the single whole latent law.

theorem sourceRoleTerm_envelope (T n g : ℕ → ℕ) (s : ℕ) (center : ℕ → ℤ)
    (globalShift : (b : ℕ) → (Fin (g b) → Bool) → Fin (T b) → ℤ)
    (b : ℕ) (bits : WindowAssignments T n g Bool (b+1)) (incoming : ℤ)
    (S : Finset (WindowLeaf T (b+1))) (a : OccupiedWindowChoice T b S)
    (F : (occupiedWindowTerm T b S a).Forced) :
    |sourceRoleTerm T n g s center globalShift b bits incoming S a|≤
      F.envelope T n g s center globalShift (occupiedTermLabels T b S a) bits incoming := by
…

Mentions: OAI.TraceReconstruction.WindowAssignments, OAI.TraceReconstruction.WindowLeaf, OAI.TraceReconstruction.OccupiedWindowChoice, OAI.TraceReconstruction.occupiedWindowTerm, OAI.TraceReconstruction.sourceRoleTerm, OAI.TraceReconstruction.occupiedTermLabels

theorem OAI.TraceReconstruction.sourceRoleAverage_envelope line 284

Source documentation

The averaged coefficient uses one exact metadata fiber. No fit event, plateau event or leaf-emission observation is conditioned on here.

theorem sourceRoleAverage_envelope (T n g : ℕ → ℕ) (s : ℕ) (center : ℕ → ℤ)
    (globalShift : (b : ℕ) → (Fin (g b) → Bool) → Fin (T b) → ℤ)
    (b : ℕ) (d : WindowAssignments T n g (Option Bool) (b+1)) (incoming : ℤ)
    (S : Finset (WindowLeaf T (b+1))) (a : OccupiedWindowChoice T b S)
    (F : (occupiedWindowTerm T b S a).Forced) :
    |sourceRoleAverage T n g s center globalShift b d incoming S a|≤
      F.averagedEnvelope T n g s center globalShift (occupiedTermLabels T b S a) d incoming := by
…

theorem OAI.TraceReconstruction.occupiedWindowTerm_leafCount line 304
theorem OAI.TraceReconstruction.occupiedWindowTerm_occupied line 310
abbrev OAI.TraceReconstruction.DegreeForcedShape line 318
Source documentation
Only the unlabeled ordered role shape is selected here; no child label or hidden orientation enters the forced choice.
```
abbrev DegreeForcedShape (b r : ℕ) :=
…
```
instance OAI.TraceReconstruction.degreeForcedShapeFinite line 321
instance OAI.TraceReconstruction.degreeForcedShapeFintype line 329
def OAI.TraceReconstruction.DegreeForcedShape.forced line 332
theorem OAI.TraceReconstruction.card_degreeForcedShape_le line 335
abbrev OAI.TraceReconstruction.SourceRoleIndex line 346
abbrev OAI.TraceReconstruction.DegreeForcedRole line 349
def OAI.TraceReconstruction.DegreeForcedRole.shape line 352
def OAI.TraceReconstruction.DegreeForcedRole.encoding line 363
theorem OAI.TraceReconstruction.DegreeForcedRole.encoding_injective line 367

def OAI.TraceReconstruction.degreeForcedRoleEnergy line 386

Source documentation

A degree-r sum over the genuine pairs (selected leaves, roles), restricted only by deterministic allowed forced labels.

def degreeForcedRoleEnergy (T n g : ℕ → ℕ) (s : ℕ) (center : ℕ → ℤ)
    (globalShift : (b : ℕ) → (Fin (g b) → Bool) → Fin (T b) → ℤ)
    (A : (b : ℕ) → Finset (Fin (T b))) (b r : ℕ)
    (d : WindowAssignments T n g (Option Bool) (b+1)) (incoming : ℤ) : ℝ :=
…

Mentions: OAI.TraceReconstruction.WindowAssignments

theorem OAI.TraceReconstruction.degreeForcedRoleEnergy_le_envelopes line 398

Source documentation

The actual coefficient indices inject into shape+numeric-labels. Thus summing the enlarged envelope really bounds the original coefficient sum, with no identification of different selected monomials.

theorem degreeForcedRoleEnergy_le_envelopes (T n g : ℕ → ℕ) (s : ℕ) (center : ℕ → ℤ)
    (globalShift : (b : ℕ) → (Fin (g b) → Bool) → Fin (T b) → ℤ)
    (A : (b : ℕ) → Finset (Fin (T b))) (b r : ℕ)
    (d : WindowAssignments T n g (Option Bool) (b+1)) (incoming : ℤ) :
    degreeForcedRoleEnergy T n g s center globalShift A b r d incoming ≤
      ∑t : DegreeForcedShape (b+1) r, ∑x : t.val.Labels T,
        if BinaryWindowLabels.allowed T A s (b+1) (t.forced.labels T x) then
          (t.forced.averagedEnvelope T n g s center globalShift x d incoming)^2 else 0 := by
…

Mentions: OAI.TraceReconstruction.WindowAssignments, OAI.TraceReconstruction.degreeForcedRoleEnergy, OAI.TraceReconstruction.DegreeForcedShape, OAI.TraceReconstruction.BinaryWindowLabels.allowed

def OAI.TraceReconstruction.interiorLabelBudget line 431
Source documentation
Uniform arithmetic interior-label budget of a degree-r depth-(b+1) shape. This includes no factor for a bottom label.
```
def interiorLabelBudget (T : ℕ → ℕ) (b r : ℕ) : ℝ :=
…
```
theorem OAI.TraceReconstruction.degreeForcedRoleEnergy_bound line 434
theorem OAI.TraceReconstruction.occupiedWindowChoice_card_le line 487
Source documentation
Total role multiplicity for one actual selected monomial. Every level has at most the number of selected leaves; no ambient-label factor occurs.
```
theorem occupiedWindowChoice_card_le (T : ℕ → ℕ) (b : ℕ)
    (S : Finset (WindowLeaf T (b+1))) :
    Fintype.card (OccupiedWindowChoice T b S) ≤ 3^((b+1)*S.card) := by
…
```
Mentions: OAI.TraceReconstruction.WindowLeaf, OAI.TraceReconstruction.OccupiedWindowChoice
abbrev OAI.TraceReconstruction.DegreeLeafSubset line 514
theorem OAI.TraceReconstruction.degreeLeafSubset_card line 517

def OAI.TraceReconstruction.SourceCentral line 538

Source documentation

All actual motif support lies in the chosen central interval at every vertex of the full window tree. This is a predicate of the complete bits, not an event on which any posterior law is conditioned.

def SourceCentral (T n g : ℕ → ℕ) (s : ℕ) (center : ℕ → ℤ)
    (globalShift : (b : ℕ) → (Fin (g b) → Bool) → Fin (T b) → ℤ)
    (A : (b : ℕ) → Finset (Fin (T b))) :
    (b : ℕ) → WindowAssignments T n g Bool b → ℤ → Prop
  | 0, _, _ => True
  | b+1, bits, incoming =>
      (∀h : Fin (T b), motifIndicator s ((h.val:ℤ)-center b+
        (∑i,(bitIndex (bits.1 i):ℤ))+incoming)≠0 → h∈A b) ∧
      ∀h, SourceCentral T n g s center globalShift A b (bits.2.2 h) (globalShift b bits.2.1 h)

Mentions: OAI.TraceReconstruction.WindowAssignments, OAI.TraceReconstruction.motifIndicator, OAI.TraceReconstruction.bitIndex

def OAI.TraceReconstruction.BinaryWindowLabels.central line 548
theorem OAI.TraceReconstruction.BinaryWindowLabels.allowed_of_central line 553
theorem OAI.TraceReconstruction.sourceRoleTerm_forced_central line 563
def OAI.TraceReconstruction.sourceNoncentralMass line 608
Source documentation
The discarded noncentral role contributions are bounded by the actual conditional probability of a failed full-tree layout. Typical metadata may bound this mass; the averaging distribution itself remains unconditional.
```
def sourceNoncentralMass (T n g : ℕ → ℕ) (s : ℕ) (center : ℕ → ℤ)
    (globalShift : (b : ℕ) → (Fin (g b) → Bool) → Fin (T b) → ℤ)
    (A : (b : ℕ) → Finset (Fin (T b))) (b : ℕ)
    (d : WindowAssignments T n g (Option Bool) b) (incoming : ℤ) : ℝ :=
…
```
Mentions: OAI.TraceReconstruction.WindowAssignments
theorem OAI.TraceReconstruction.sourceNoncentralMass_nonneg line 615
theorem OAI.TraceReconstruction.sourceRoleAverage_not_allowed line 623
theorem OAI.TraceReconstruction.sum_subtype_zero_extend line 657
Source documentation
Extension by zero commutes with the finite subtype sum, including an empty subtype and predicates depending on dependent role indices.
```
theorem sum_subtype_zero_extend {α : Type*} [Fintype α] (p : α → Prop) [DecidablePred p]
    (f : {x // p x} → ℝ) :
    (∑x, if h : p x then f ⟨x,h⟩ else 0) = ∑x,f x := by
…
```

def OAI.TraceReconstruction.sourceCoefficient line 672

Source documentation

The coefficient is defined directly from the two literal leaf-type patterns under the common complete posterior bit tree.

def sourceCoefficient (T n g : ℕ → ℕ) (s : ℕ) (center : ℕ → ℤ)
    (globalShift : (b : ℕ) → (Fin (g b) → Bool) → Fin (T b) → ℤ)
    (b : ℕ) (d : WindowAssignments T n g (Option Bool) (b+1)) (incoming : ℤ)
    (S : Finset (WindowLeaf T (b+1))) : ℝ :=
…

Mentions: OAI.TraceReconstruction.WindowAssignments, OAI.TraceReconstruction.WindowLeaf

theorem OAI.TraceReconstruction.sourceCoefficient_expansion line 681
def OAI.TraceReconstruction.sourceGoodRoleSquare line 693
theorem OAI.TraceReconstruction.sourceGoodRoleSquare_nonneg line 705
theorem OAI.TraceReconstruction.sourceGoodRoleSquare_sum line 714

theorem OAI.TraceReconstruction.sourceRoleSquare_split line 730

Source documentation

Every actual odd role term is either smoothed at an actual singleton, discarded by the literal central-layout failure event, or retained in the forced-tree sum. There is no unproved coefficient-bound assumption.

theorem sourceRoleSquare_split (T n g : ℕ → ℕ) (s : ℕ) (center : ℕ → ℤ)
    (globalShift : (b : ℕ) → (Fin (g b) → Bool) → Fin (T b) → ℤ)
    (A : (b : ℕ) → Finset (Fin (T b))) (b r : ℕ)
    (d : WindowAssignments T n g (Option Bool) (b+1)) (incoming : ℤ)
    (S : Finset (WindowLeaf T (b+1))) (hS : S.card=r) (a : OccupiedWindowChoice T b S)
    (η : ℝ) (hcap : MetadataSmoothingCap T n g s η (b+1) d) :
    (if (occupiedWindowTerm T b S a).isOdd then
      sourceRoleAverage T n g s center globalShift b d incoming S a else 0)^2 ≤
      η^2+(sourceNoncentralMass T n g s center globalShift A (b+1) d incoming)^2+
        sourceGoodRoleSquare T n g s center globalShift A b r d incoming ⟨S,a⟩ := by
…

Mentions: OAI.TraceReconstruction.WindowAssignments, OAI.TraceReconstruction.WindowLeaf, OAI.TraceReconstruction.OccupiedWindowChoice, OAI.TraceReconstruction.MetadataSmoothingCap, OAI.TraceReconstruction.occupiedWindowTerm, OAI.TraceReconstruction.sourceRoleAverage, OAI.TraceReconstruction.sourceNoncentralMass, OAI.TraceReconstruction.sourceGoodRoleSquare

theorem OAI.TraceReconstruction.sourceGoodRoleSquare_degree_sum line 778
theorem OAI.TraceReconstruction.sourceCoefficient_square_bound line 801

theorem OAI.TraceReconstruction.sourceCoefficient_degree_energy line 844

Source documentation

The full degree coefficient sum, including every selected monomial, singletons, and off-center labels. This is the finite, unabsorbed version of the manuscript's low-degree coefficient estimate.

theorem sourceCoefficient_degree_energy (T n g : ℕ → ℕ) (s : ℕ) (center : ℕ → ℤ)
    (globalShift : (b : ℕ) → (Fin (g b) → Bool) → Fin (T b) → ℤ)
    (A : (b : ℕ) → Finset (Fin (T b))) (b r : ℕ)
    (d : WindowAssignments T n g (Option Bool) (b+1)) (incoming : ℤ)
    (η : ℝ) (hcap : MetadataSmoothingCap T n g s η (b+1) d) :
    (∑S : DegreeLeafSubset T b r,
      (sourceCoefficient T n g s center globalShift b d incoming S.val)^2) ≤
      4*(3^((b+1)*r):ℕ)*
        (((Fintype.card (WindowLeaf T (b+1))).choose r:ℕ)*(3^((b+1)*r):ℕ)*
          (η^2+(sourceNoncentralMass T n g s center globalShift A (b+1) d incoming)^2)+
          degreeForcedRoleEnergy T n g s center globalShift A b r d incoming) := by
…

Mentions: OAI.TraceReconstruction.WindowAssignments, OAI.TraceReconstruction.MetadataSmoothingCap, OAI.TraceReconstruction.DegreeLeafSubset, OAI.TraceReconstruction.sourceCoefficient, OAI.TraceReconstruction.WindowLeaf, OAI.TraceReconstruction.sourceNoncentralMass, OAI.TraceReconstruction.degreeForcedRoleEnergy