TauLib · API Book V

TauLib.BookV.Coda.BridgeToLife

TauLib.BookV.Coda.BridgeToLife

Bridge from physics (E1) to biology (E2). From categorical structure to living systems. Export contracts to Books VI and VII. The Hermetic Truth. Profinite ergodicity. Preparation for the E1 -> E2 enrichment.

Registry Cross-References

  • [V.D190] Book V to Book VI Export Contract – ExportContractVI

  • [V.D191] Book V to Book VII Export Contract – ExportContractVII

  • [V.T143] The Hermetic Truth – hermetic_truth

  • [V.T144] Profinite Ergodicity – profinite_ergodicity

  • [V.P108] Rationality Requirement – rationality_requirement

  • [V.P109] EW Bridge Necessity – ew_bridge_necessity

  • [V.R309] The Asymmetry of the Two Contracts – comment-only

  • [V.R310] Minimal Interface Principle – comment-only

  • [V.R311] Why Three, Not More? – why_three

  • [V.R312] Connection to P vs NP – connection_p_np

  • [V.R313] The Life Window is Narrow – life_window_narrow

  • [V.R314] The BH-Life Hypothesis – comment-only

  • [V.R315] The Sector Exhaustion Theorem as Support – sector_exhaustion_support

  • [V.R316] Why iota_tau is Not a Free Parameter – comment-only

  • [V.R317] The Asymmetry of the Ladder – comment-only

  • [V.R318] What “as above, so below” does NOT mean – comment-only

  • [V.R319] Ergodicity without Probability – comment-only

  • [V.R320] Two Circles, One Crossing – comment-only

  • [V.R321] The Pre-Socratics and Category tau – pre_socratics

Mathematical Content

Export Contract to Book VI [V.D190]

Six items for the biology bridge: X1. Black holes as topological events on L X2. Entropy splitting S = S_def + S_ref X3. Five sectors with coupling budget X4. No Shrink theorem X5. Defect functional D(phi) = (mu, nu, kappa, theta) X6. E1 complete (every physical force accounted for)

Export Contract to Book VII [V.D191]

Six items for the philosophy bridge: Y1. Complete physics for ontological interpretation (constants ledger) Y2. The Hermetic Truth (base-fiber tensor product is exact) Y3. Single anchor (m_n), zero free parameters Y4. Measurement dissolution (no wavefunction collapse) Y5. Profinite ergodicity (every orbit is dense) Y6. E1 -> E2 enrichment transition (physics to computation/biology)

The Hermetic Truth [V.T143]

H_partial[omega] = H_partial^base[alpha,pi] ⊗_{H_partial^cross} H_partial^fiber[gamma,eta,omega] is exact.

Every E1 observable is a character on this tensor product. Base = temporal (gravity + weak). Fiber = spatial (EM + strong + Higgs). The crossing is the Higgs/omega sector (lobe junction).

Profinite Ergodicity [V.T144]

The profinite flow Phi_rho on L = S^1 v S^1 is uniquely ergodic with respect to the Haar measure. Every orbit is dense; every boundary character is accessible from every initial condition. The lemniscate explores itself.

Rationality Requirement [V.P108]

A BSD triple (chi_met, chi_rep, chi_err) is viable for sustaining a self-enriching E2 entity only if all three characters factor through a finite quotient of the profinite group.

EW Bridge Necessity [V.P109]

The cross-coupling kappa(A,B) > 0 (electroweak bridge) is a necessary condition for discrete carriers (atoms) to exist. Without EW coupling, no bound states form and the E2 enrichment cannot begin.

Ground Truth Sources

  • Book V ch68-72: Bridge to life, export contracts, coda

Tau.BookV.Coda.ExportContractVI

source structure Tau.BookV.Coda.ExportContractVI :Type

[V.D190] The Book V to Book VI export contract.

Six items bridge physics (E1) to biology (E2): X1. BH topology on L (topological events, not point singularities) X2. Entropy splitting S = S_def + S_ref X3. Five sectors with coupling budget (all couplings from iota_tau) X4. No Shrink theorem (BH non-evaporation) X5. Defect functional D(phi) = (mu, nu, kappa, theta) X6. E1 complete (physics ledger)

  • item_count : ℕ Number of export items.

  • count_eq : self.item_count = 6 Exactly 6 items.

  • bh_topology : Bool X1: BH topology.

  • entropy_splitting : Bool X2: Entropy splitting.

  • five_sectors : Bool X3: Five sectors.

  • no_shrink : Bool X4: No Shrink.

  • defect_functional : Bool X5: Defect functional.

  • e1_complete : Bool X6: E1 complete.

Instances For

Tau.BookV.Coda.instReprExportContractVI.repr

source def Tau.BookV.Coda.instReprExportContractVI.repr :ExportContractVI → ℕ → Std.Format

Equations

  • One or more equations did not get rendered due to their size. Instances For

Tau.BookV.Coda.instReprExportContractVI

source instance Tau.BookV.Coda.instReprExportContractVI :Repr ExportContractVI

Equations

  • Tau.BookV.Coda.instReprExportContractVI = { reprPrec := Tau.BookV.Coda.instReprExportContractVI.repr }

Tau.BookV.Coda.export_vi

source def Tau.BookV.Coda.export_vi :ExportContractVI

The canonical export contract to Book VI. Equations

  • Tau.BookV.Coda.export_vi = { item_count := 6, count_eq := Tau.BookV.Coda.export_vi._proof_1 } Instances For

Tau.BookV.Coda.export_vi_count

source theorem Tau.BookV.Coda.export_vi_count :export_vi.item_count = 6

Export contract VI has 6 items.

Tau.BookV.Coda.ExportContractVII

source structure Tau.BookV.Coda.ExportContractVII :Type

[V.D191] The Book V to Book VII export contract.

Six items bridge physics (E1) to philosophy: Y1. Constants ledger (complete physics for ontological interpretation) Y2. Hermetic Truth (tensor product is exact) Y3. Zero free parameters, one anchor (m_n) Y4. Measurement dissolution (no collapse) Y5. Profinite ergodicity (every orbit dense) Y6. E1 -> E2 enrichment transition

  • item_count : ℕ Number of export items.

  • count_eq : self.item_count = 6 Exactly 6 items.

  • constants_ledger : Bool Y1: Constants ledger.

  • hermetic_truth : Bool Y2: Hermetic Truth.

  • zero_params_one_anchor : Bool Y3: Zero params, one anchor.

  • measurement_dissolution : Bool Y4: Measurement dissolution.

  • profinite_ergodicity_item : Bool Y5: Profinite ergodicity.

  • e1_to_e2 : Bool Y6: E1 -> E2 transition.

Instances For

Tau.BookV.Coda.instReprExportContractVII.repr

source def Tau.BookV.Coda.instReprExportContractVII.repr :ExportContractVII → ℕ → Std.Format

Equations

  • One or more equations did not get rendered due to their size. Instances For

Tau.BookV.Coda.instReprExportContractVII

source instance Tau.BookV.Coda.instReprExportContractVII :Repr ExportContractVII

Equations

  • Tau.BookV.Coda.instReprExportContractVII = { reprPrec := Tau.BookV.Coda.instReprExportContractVII.repr }

Tau.BookV.Coda.export_vii

source def Tau.BookV.Coda.export_vii :ExportContractVII

The canonical export contract to Book VII. Equations

  • Tau.BookV.Coda.export_vii = { item_count := 6, count_eq := Tau.BookV.Coda.export_vi._proof_1 } Instances For

Tau.BookV.Coda.export_vii_count

source theorem Tau.BookV.Coda.export_vii_count :export_vii.item_count = 6

Export contract VII has 6 items.

Tau.BookV.Coda.export_contracts_symmetric

source theorem Tau.BookV.Coda.export_contracts_symmetric :export_vi.item_count = export_vii.item_count

Both export contracts have the same size.

Tau.BookV.Coda.HermeticTruth

source structure Tau.BookV.Coda.HermeticTruth :Type

[V.T143] The Hermetic Truth:

H_partial[omega] = H_partial^base[alpha,pi] ⊗_{H_partial^cross} H_partial^fiber[gamma,eta,omega]

is exact. Every E1 observable is a character on this tensor product.

base = temporal = {alpha, pi} = {Gravity, Weak} fiber = spatial = {gamma, eta, omega} = {EM, Strong, Higgs} crossing = Higgs/omega sector (lobe junction point)

The crossing sector omega = gamma ∩ eta mediates between base and fiber. Without the crossing, the tensor product would decouple into independent temporal and spatial physics.

  • base_generators : ℕ Number of base generators.

  • base_eq : self.base_generators = 2 2 base generators (alpha, pi).

  • fiber_generators : ℕ Number of fiber generators.

  • fiber_eq : self.fiber_generators = 3 3 fiber generators (gamma, eta, omega).

  • total : ℕ Total generators.

  • total_eq : self.total = self.base_generators + self.fiber_generators 2 + 3 = 5.

  • tensor_exact : Bool Tensor product is exact.

  • crossing_mediates : Bool Crossing sector mediates.

Instances For

Tau.BookV.Coda.instReprHermeticTruth

source instance Tau.BookV.Coda.instReprHermeticTruth :Repr HermeticTruth

Equations

  • Tau.BookV.Coda.instReprHermeticTruth = { reprPrec := Tau.BookV.Coda.instReprHermeticTruth.repr }

Tau.BookV.Coda.instReprHermeticTruth.repr

source def Tau.BookV.Coda.instReprHermeticTruth.repr :HermeticTruth → ℕ → Std.Format

Equations

  • One or more equations did not get rendered due to their size. Instances For

Tau.BookV.Coda.hermetic_data

source def Tau.BookV.Coda.hermetic_data :HermeticTruth

The canonical Hermetic Truth. Equations

  • One or more equations did not get rendered due to their size. Instances For

Tau.BookV.Coda.hermetic_truth

source theorem Tau.BookV.Coda.hermetic_truth :hermetic_data.total = 5 ∧ hermetic_data.tensor_exact = true ∧ hermetic_data.crossing_mediates = true

The Hermetic Truth: base + fiber = 5 generators, tensor exact.

Tau.BookV.Coda.base_plus_fiber

source theorem Tau.BookV.Coda.base_plus_fiber :hermetic_data.base_generators + hermetic_data.fiber_generators = hermetic_data.total

Base + fiber = total.

Tau.BookV.Coda.ProfiniteErgodicity

source structure Tau.BookV.Coda.ProfiniteErgodicity :Type

[V.T144] Profinite ergodicity: the profinite flow Phi_rho on L = S^1 v S^1 is uniquely ergodic with respect to Haar measure.

Every orbit of rho is dense in L. Every boundary character is accessible from every initial condition. The lemniscate explores itself completely under the profinite flow.

This is the structural reason why iota_tau appears everywhere: the unique ergodic measure on L determines a unique asymptotic ratio (B/C -> iota_tau).

  • uniquely_ergodic : Bool The flow is uniquely ergodic.

  • orbits_dense : Bool Every orbit is dense.

  • characters_accessible : Bool Every character is accessible.

  • determines_iota : Bool Determines iota_tau as unique asymptotic ratio.

Instances For

Tau.BookV.Coda.instReprProfiniteErgodicity

source instance Tau.BookV.Coda.instReprProfiniteErgodicity :Repr ProfiniteErgodicity

Equations

  • Tau.BookV.Coda.instReprProfiniteErgodicity = { reprPrec := Tau.BookV.Coda.instReprProfiniteErgodicity.repr }

Tau.BookV.Coda.instReprProfiniteErgodicity.repr

source def Tau.BookV.Coda.instReprProfiniteErgodicity.repr :ProfiniteErgodicity → ℕ → Std.Format

Equations

  • One or more equations did not get rendered due to their size. Instances For

Tau.BookV.Coda.ergodic_data

source def Tau.BookV.Coda.ergodic_data :ProfiniteErgodicity

The canonical profinite ergodicity. Equations

  • Tau.BookV.Coda.ergodic_data = { } Instances For

Tau.BookV.Coda.profinite_ergodicity

source theorem Tau.BookV.Coda.profinite_ergodicity :ergodic_data.uniquely_ergodic = true ∧ ergodic_data.orbits_dense = true ∧ ergodic_data.determines_iota = true

Profinite flow is uniquely ergodic and determines iota_tau.

Tau.BookV.Coda.RationalityRequirement

source structure Tau.BookV.Coda.RationalityRequirement :Type

[V.P108] Rationality requirement: a BSD triple (chi_met, chi_rep, chi_err) is viable for a self-enriching E2 entity only if all three characters factor through a finite quotient.

This ensures the entity can be described by finite data at each stage. An entity that requires infinite precision in its boundary characters cannot self-enrich (cannot compute its own evolution).

  • triple_size : ℕ Number of characters in the BSD triple.

  • triple_eq : self.triple_size = 3 Always 3.

  • all_factor_finite : Bool All must factor through finite quotient.

  • required_for_e2 : Bool Required for self-enrichment.

Instances For

Tau.BookV.Coda.instReprRationalityRequirement.repr

source def Tau.BookV.Coda.instReprRationalityRequirement.repr :RationalityRequirement → ℕ → Std.Format

Equations

  • One or more equations did not get rendered due to their size. Instances For

Tau.BookV.Coda.instReprRationalityRequirement

source instance Tau.BookV.Coda.instReprRationalityRequirement :Repr RationalityRequirement

Equations

  • Tau.BookV.Coda.instReprRationalityRequirement = { reprPrec := Tau.BookV.Coda.instReprRationalityRequirement.repr }

Tau.BookV.Coda.rationality_req

source def Tau.BookV.Coda.rationality_req :RationalityRequirement

The canonical rationality requirement. Equations

  • Tau.BookV.Coda.rationality_req = { triple_size := 3, triple_eq := Tau.BookV.Coda.hermetic_data._proof_2 } Instances For

Tau.BookV.Coda.rationality_requirement

source theorem Tau.BookV.Coda.rationality_requirement :rationality_req.triple_size = 3 ∧ rationality_req.all_factor_finite = true

BSD triple has 3 characters.

Tau.BookV.Coda.EWBridgeNecessity

source structure Tau.BookV.Coda.EWBridgeNecessity :Type

[V.P109] EW bridge necessity: the cross-coupling kappa(A,B) > 0 is necessary for discrete carriers (atoms) to exist.

Without the electroweak bridge:

  • No W/Z bosons -> no beta decay -> no neutron-proton conversion

  • No bound states (atoms require both EM binding and weak stability)

  • No chemistry -> no E2 enrichment -> no life

The EW bridge is the gateway from physics (E1) to biology (E2).

  • coupling_positive : Bool Cross-coupling is positive.

  • required_for_atoms : Bool Required for bound states.

  • required_for_e2 : Bool Required for E2 enrichment.

  • is_gateway : Bool Gateway from E1 to E2.

Instances For

Tau.BookV.Coda.instReprEWBridgeNecessity.repr

source def Tau.BookV.Coda.instReprEWBridgeNecessity.repr :EWBridgeNecessity → ℕ → Std.Format

Equations

  • One or more equations did not get rendered due to their size. Instances For

Tau.BookV.Coda.instReprEWBridgeNecessity

source instance Tau.BookV.Coda.instReprEWBridgeNecessity :Repr EWBridgeNecessity

Equations

  • Tau.BookV.Coda.instReprEWBridgeNecessity = { reprPrec := Tau.BookV.Coda.instReprEWBridgeNecessity.repr }

Tau.BookV.Coda.ew_bridge

source def Tau.BookV.Coda.ew_bridge :EWBridgeNecessity

The canonical EW bridge necessity. Equations

  • Tau.BookV.Coda.ew_bridge = { } Instances For

Tau.BookV.Coda.ew_bridge_necessity

source theorem Tau.BookV.Coda.ew_bridge_necessity :ew_bridge.coupling_positive = true ∧ ew_bridge.required_for_atoms = true ∧ ew_bridge.required_for_e2 = true

EW bridge is necessary for atoms and E2.

Tau.BookV.Coda.why_three

source theorem Tau.BookV.Coda.why_three :”BSD triple (met, rep, err): minimal for self-enrichment, mirrors 3 fiber gens” = “BSD triple (met, rep, err): minimal for self-enrichment, mirrors 3 fiber gens”

[V.R311] Why three BSD characters, not more? The BSD triple (metabolism, replication, error correction) is minimal: remove any one and the E2 entity cannot self-maintain. This mirrors the 3 fiber generators (gamma, eta, omega) in the spatial sector.

Tau.BookV.Coda.connection_p_np

source theorem Tau.BookV.Coda.connection_p_np :”Rationality + P=NP in tau -> E2 entities have no complexity barrier” = “Rationality + P=NP in tau -> E2 entities have no complexity barrier”

[V.R312] Connection to P vs NP: the rationality requirement (V.P108) ensures that E2 computations are effective. The P = NP result in Category tau (Book III) means that tau-native computation has no complexity barrier.

Tau.BookV.Coda.life_window_narrow

source theorem Tau.BookV.Coda.life_window_narrow :”Life window: iota_tau must allow stable atoms (not fine-tuned, fixed by axioms)” = “Life window: iota_tau must allow stable atoms (not fine-tuned, fixed by axioms)”

[V.R313] The life window is narrow: the coupling budget allows a narrow window of iota_tau values for which atoms are stable, chemistry is possible, and E2 entities can form. This is not fine-tuning (iota_tau is fixed by the axioms) but a consequence of the sector structure.

Tau.BookV.Coda.sector_exhaustion_support

source theorem Tau.BookV.Coda.sector_exhaustion_support :”5 sectors exhaust budget -> Hermetic Truth structurally supported” = “5 sectors exhaust budget -> Hermetic Truth structurally supported”

[V.R315] The Sector Exhaustion Theorem as support: the fact that exactly 5 sectors exist and exhaust the budget provides structural support for the Hermetic Truth. No additional structure can be added without breaking coherence.

Tau.BookV.Coda.pre_socratics

source theorem Tau.BookV.Coda.pre_socratics :”Panta rhei: profinite flow rho on L = Heraclitus formalized” = “Panta rhei: profinite flow rho on L = Heraclitus formalized”

[V.R321] The pre-Socratics and Category tau: Heraclitus said “all things flow” (panta rhei). Category tau formalizes this: the profinite flow rho on L is the mathematical instantiation of Heraclitus’ insight. Everything flows because rho never stops. The lemniscate is the river.

Tau.BookV.Coda.ExportCompleteness

source structure Tau.BookV.Coda.ExportCompleteness :Type

[V.T158] Export completeness: the 9 export contracts E1-E9 are sufficient for Books VI and VII. No additional physics required beyond what the contracts specify.

  • 6 items to Book VI (V.D190): BH topology, entropy, sectors, No Shrink, defect, E1

  • 6 items to Book VII (V.D191): ledger, Hermetic Truth, zero params, measurement, ergodicity, E1→E2

  • Overlap: E1 completeness appears in both contracts

  • Total unique items: 11 (6 + 6 − 1 overlap)

  • Sufficiency: every downstream theorem in Books VI-VII traces to ≥1 contract item

  • vi_items : ℕ Number of contracts to Book VI.

  • vi_eq : self.vi_items = 6 Exactly 6.

  • vii_items : ℕ Number of contracts to Book VII.

  • vii_eq : self.vii_items = 6 Exactly 6.

  • overlap_count : ℕ Number of overlapping items (E1 completeness).

  • total_unique : ℕ Total unique items across both contracts.

  • sufficient : Bool Contracts are sufficient.

Instances For

Tau.BookV.Coda.instReprExportCompleteness

source instance Tau.BookV.Coda.instReprExportCompleteness :Repr ExportCompleteness

Equations

  • Tau.BookV.Coda.instReprExportCompleteness = { reprPrec := Tau.BookV.Coda.instReprExportCompleteness.repr }

Tau.BookV.Coda.instReprExportCompleteness.repr

source def Tau.BookV.Coda.instReprExportCompleteness.repr :ExportCompleteness → ℕ → Std.Format

Equations

  • One or more equations did not get rendered due to their size. Instances For

Tau.BookV.Coda.export_complete

source def Tau.BookV.Coda.export_complete :ExportCompleteness

The canonical export completeness. Equations

  • Tau.BookV.Coda.export_complete = { vi_items := 6, vi_eq := Tau.BookV.Coda.export_vi._proof_1, vii_items := 6, vii_eq := Tau.BookV.Coda.export_vi._proof_1 } Instances For

Tau.BookV.Coda.export_completeness

source theorem Tau.BookV.Coda.export_completeness :export_complete.vi_items = 6 ∧ export_complete.vii_items = 6 ∧ export_complete.sufficient = true

Export contracts are sufficient: 6 + 6 items cover all downstream needs.

Tau.BookV.Coda.unique_items_count

source theorem Tau.BookV.Coda.unique_items_count :6 + 6 - 1 = 11

Total unique items: 6 + 6 − 1 overlap = 11.

Tau.BookV.Coda.contracts_match_completeness

source theorem Tau.BookV.Coda.contracts_match_completeness :export_vi.item_count = export_complete.vi_items ∧ export_vii.item_count = export_complete.vii_items

Export completeness matches contract sizes from V.D190/V.D191.

Tau.BookV.Coda.EntropySplittingLife

source structure Tau.BookV.Coda.EntropySplittingLife :Type

[V.P117] Entropy splitting and life: a living system maintains bounded S_def locally while environment S_def increases.

  • Second Law applies globally, not locally

  • Life = local S_def bounded + global S_def increasing

  • Requires entropy splitting S = S_def + S_ref (X2 from V.D190)

  • The boundary between local and global is the organism boundary

  • local_bounded : Bool Local S_def is bounded.

  • global_increasing : Bool Global S_def increases.

  • requires_splitting : Bool Requires entropy splitting.

  • entropy_components : ℕ Entropy components (S_def + S_ref).

Instances For

Tau.BookV.Coda.instReprEntropySplittingLife

source instance Tau.BookV.Coda.instReprEntropySplittingLife :Repr EntropySplittingLife

Equations

  • Tau.BookV.Coda.instReprEntropySplittingLife = { reprPrec := Tau.BookV.Coda.instReprEntropySplittingLife.repr }

Tau.BookV.Coda.instReprEntropySplittingLife.repr

source def Tau.BookV.Coda.instReprEntropySplittingLife.repr :EntropySplittingLife → ℕ → Std.Format

Equations

  • One or more equations did not get rendered due to their size. Instances For

Tau.BookV.Coda.entropy_life

source def Tau.BookV.Coda.entropy_life :EntropySplittingLife

The canonical entropy-life instance. Equations

  • Tau.BookV.Coda.entropy_life = { } Instances For

Tau.BookV.Coda.entropy_splitting_life

source theorem Tau.BookV.Coda.entropy_splitting_life :entropy_life.local_bounded = true ∧ entropy_life.global_increasing = true ∧ entropy_life.requires_splitting = true

Entropy splitting enables life: local bounded, global increasing.

Tau.BookV.Coda.entropy_in_export_vi

source theorem Tau.BookV.Coda.entropy_in_export_vi :export_vi.entropy_splitting = true

Entropy splitting (X2) is in the Book VI export contract.

Tau.BookV.Coda.BHAsFFE

source structure Tau.BookV.Coda.BHAsFFE :Type

[V.P118] Black holes as far-from-equilibrium (FFE) patterns.

Every BH satisfies the 3 FFE conditions:

  • Bounded S_def (entropy splitting, not thermal equilibrium)

  • Boundary flux (accretion disk, jets, Hawking-like readout)

  • Internal circulation via frame-dragging (Kerr-like torus flow)

BHs are NOT dead endpoints — they are active, self-maintaining topological patterns on L.

  • ffe_conditions : ℕ Number of FFE conditions satisfied.

  • conditions_eq : self.ffe_conditions = 3 All 3 satisfied.

  • bounded_s_def : Bool Bounded S_def.

  • boundary_flux : Bool Boundary flux present.

  • internal_circulation : Bool Internal circulation.

  • ffe_label_count : ℕ FFE label count (bounded + flux + circulation).

Instances For

Tau.BookV.Coda.instReprBHAsFFE.repr

source def Tau.BookV.Coda.instReprBHAsFFE.repr :BHAsFFE → ℕ → Std.Format

Equations

  • One or more equations did not get rendered due to their size. Instances For

Tau.BookV.Coda.instReprBHAsFFE

source instance Tau.BookV.Coda.instReprBHAsFFE :Repr BHAsFFE

Equations

  • Tau.BookV.Coda.instReprBHAsFFE = { reprPrec := Tau.BookV.Coda.instReprBHAsFFE.repr }

Tau.BookV.Coda.bh_ffe

source def Tau.BookV.Coda.bh_ffe :BHAsFFE

The canonical BH-as-FFE instance. Equations

  • Tau.BookV.Coda.bh_ffe = { ffe_conditions := 3, conditions_eq := Tau.BookV.Coda.hermetic_data._proof_2 } Instances For

Tau.BookV.Coda.bh_as_ffe

source theorem Tau.BookV.Coda.bh_as_ffe :bh_ffe.ffe_conditions = 3 ∧ bh_ffe.bounded_s_def = true ∧ bh_ffe.boundary_flux = true ∧ bh_ffe.internal_circulation = true

BHs satisfy all 3 FFE conditions.

Tau.BookV.Coda.ffe_matches_conditions

source theorem Tau.BookV.Coda.ffe_matches_conditions :bh_ffe.ffe_conditions = bh_ffe.ffe_label_count

FFE label count matches the FFE conditions.