Chosen growths as ordered growths

Converts a chosen growth — one following the active-extension choice system — into an ordinary ordered growth certificate, and identifies the branch integrals, interpolation points, and integrands of the grown and canonical forests with the intrinsic ordered-contribution data of those forests.

theorem BKAR.Forest.ChosenGrowth.exists_orderedGrowth {V : Type u_1} [Fintype V] [DecidableEq V] {choices : ActiveExtensionChoice V} {F G : Forest V} {order : List (Edge V)} (path : ChosenGrowth choices F order G) : Nonempty (F.OrderedGrowth order G)

A chosen growth path is, in particular, an ordered growth certificate with the same edge order and terminal forest.

noncomputable def BKAR.Forest.ChosenGrowth.toOrderedGrowth {V : Type u_1} [Fintype V] [DecidableEq V] {choices : ActiveExtensionChoice V} {F G : Forest V} {order : List (Edge V)} (path : ChosenGrowth choices F order G) : F.OrderedGrowth order G

A definite ordered-growth certificate obtained from a chosen growth path. This is only a certificate extractor; mathematical identities below do not depend on the particular proof object chosen.

Equations

• path.toOrderedGrowth = Classical.choice ⋯

theorem BKAR.Forest.OrderedGrowth.branchIntegral_emptyStart_eq_orderedContribution {V : Type u_1} [Fintype V] [DecidableEq V] {G : Forest V} {order : List (Edge V)} (growth : (empty V).OrderedGrowth order G) (ρ : (Edge V → ℝ) → ℝ) : growth.branchIntegral emptyParam ρ = G.orderedContribution order ρ

An ordered growth from the empty forest computes the same integral as the ordered contribution of its terminal Forest representative in that growth order.

theorem BKAR.Forest.ChosenGrowth.branchIntegral_emptyStart_eq_orderedContribution {V : Type u_1} [Fintype V] [DecidableEq V] {choices : ActiveExtensionChoice V} {G : Forest V} {order : List (Edge V)} (path : ChosenGrowth choices (empty V) order G) (ρ : (Edge V → ℝ) → ℝ) : path.toOrderedGrowth.branchIntegral emptyParam ρ = G.orderedContribution order ρ

Chosen-growth version of OrderedGrowth.branchIntegral_emptyStart_eq_orderedContribution.

noncomputable def BKAR.Forest.grownForestForSupportOrderGrowth {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (I : ForestIndex V) (order : ↥(edgeSetOrders I.edges)) : (empty V).OrderedGrowth (↑order) (grownForestForSupportOrder choices I order)

The ordered-growth certificate carried by a grown support/order forest.

Equations

• BKAR.Forest.grownForestForSupportOrderGrowth choices I order = ⋯.toOrderedGrowth

theorem BKAR.Forest.grownForestForSupportOrder_branchIntegral_eq_orderedContribution {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (I : ForestIndex V) (order : ↥(edgeSetOrders I.edges)) (ρ : (Edge V → ℝ) → ℝ) : (grownForestForSupportOrderGrowth choices I order).branchIntegral emptyParam ρ = (grownForestForSupportOrder choices I order).orderedContribution (↑order) ρ

The grown support/order forest's ordered contribution can be read as the branch integral of its concrete ordered-growth certificate.

theorem BKAR.Forest.grownForestForSupportOrder_branchPoint_eq_standardInterp_paramsOfOrder {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (I : ForestIndex V) (order : ↥(edgeSetOrders I.edges)) (ts : List ℝ) (hlen : ts.length = (↑order).length) : (grownForestForSupportOrderGrowth choices I order).branchPoint emptyParam ts = (grownForestForSupportOrder choices I order).standardInterp ((grownForestForSupportOrder choices I order).paramsOfOrder (↑order) ts)

The branch point attached to a grown support/order forest is exactly its standard interpolation in the same ordered-sector coordinates.

theorem BKAR.Forest.grownForestForSupportOrder_branchIntegrand_eq_orderedSectorIntegrand {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (I : ForestIndex V) (order : ↥(edgeSetOrders I.edges)) (ρ : (Edge V → ℝ) → ℝ) (ts : List ℝ) (hlen : ts.length = (↑order).length) : (grownForestForSupportOrderGrowth choices I order).branchIntegrand emptyParam ρ ts = mixedPartialList (↑order).reverse ρ ((grownForestForSupportOrder choices I order).standardInterp ((grownForestForSupportOrder choices I order).paramsOfOrder (↑order) ts))

The grown support/order branch integrand is the usual ordered-sector integrand of the grown Forest representative, in list simplex coordinates.

noncomputable def BKAR.Forest.canonicalGrownForestForSupportGrowth {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (I : ForestIndex V) : (empty V).OrderedGrowth (↑I.canonicalOrder) (canonicalGrownForestForSupport choices I)

The ordered-growth certificate carried by the canonical support representative.

Equations

• BKAR.Forest.canonicalGrownForestForSupportGrowth choices I = BKAR.Forest.grownForestForSupportOrderGrowth choices I I.canonicalOrder

theorem BKAR.Forest.canonicalGrownForestForSupport_branchIntegral_eq_orderedContribution {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (I : ForestIndex V) (ρ : (Edge V → ℝ) → ℝ) : (canonicalGrownForestForSupportGrowth choices I).branchIntegral emptyParam ρ = (canonicalGrownForestForSupport choices I).orderedContribution (↑I.canonicalOrder) ρ

The canonical support representative's canonical-order contribution is the branch integral of its concrete ordered-growth certificate.

theorem BKAR.Forest.canonicalGrownForestForSupport_branchPoint_eq_standardInterp_paramsOfOrder {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (I : ForestIndex V) (ts : List ℝ) (hlen : ts.length = (↑I.canonicalOrder).length) : (canonicalGrownForestForSupportGrowth choices I).branchPoint emptyParam ts = (canonicalGrownForestForSupport choices I).standardInterp ((canonicalGrownForestForSupport choices I).paramsOfOrder (↑I.canonicalOrder) ts)

The branch point attached to the canonical support representative is exactly its standard interpolation in canonical-order coordinates.

theorem BKAR.Forest.canonicalGrownForestForSupport_branchIntegrand_eq_orderedSectorIntegrand {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (I : ForestIndex V) (ρ : (Edge V → ℝ) → ℝ) (ts : List ℝ) (hlen : ts.length = (↑I.canonicalOrder).length) : (canonicalGrownForestForSupportGrowth choices I).branchIntegrand emptyParam ρ ts = mixedPartialList (↑I.canonicalOrder).reverse ρ ((canonicalGrownForestForSupport choices I).standardInterp ((canonicalGrownForestForSupport choices I).paramsOfOrder (↑I.canonicalOrder) ts))

The canonical support representative's canonical branch integrand is the usual ordered-sector integrand of that representative, in list simplex coordinates.